Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0:
In x0 (V_ x1).
Apply unknownprop_4358b1b5e793b47fce3fac2d82616bfe2f6625cb01f2397277ef761d656463ce with
x1,
λ x2 x3 . In x0 x2.
The subproof is completed by applying H0.
Apply unknownprop_6aa6a1e2972a64fa9285a0890d0ac4772ddcd8c250de1b168f8abb7d1edde683 with
x1,
λ x2 . Power (V_ x2),
x0,
∀ x2 : ο . (∀ x3 . In x3 x1 ⟶ Subq x0 (V_ x3) ⟶ x2) ⟶ x2 leaving 2 subgoals.
The subproof is completed by applying L1.
Let x2 of type ι be given.
Apply andE with
In x2 x1,
In x0 (Power (V_ x2)),
∀ x3 : ο . (∀ x4 . In x4 x1 ⟶ Subq x0 (V_ x4) ⟶ x3) ⟶ x3 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x3 of type ο be given.
Assume H5:
∀ x4 . In x4 x1 ⟶ Subq x0 (V_ x4) ⟶ x3.
Apply H5 with
x2 leaving 2 subgoals.
The subproof is completed by applying H3.
Apply unknownprop_b8811722bb772bba243207d8ee471ba24f8b88e821f7737307414168e638d2c6 with
V_ x2,
x0.
The subproof is completed by applying H4.