Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: x1 ∈ x0.
Apply atleastp_tra with
u1,
Sing x1,
x0 leaving 2 subgoals.
Apply equip_atleastp with
u1,
Sing x1.
Apply equip_sym with
Sing x1,
u1.
The subproof is completed by applying unknownprop_be1ab2772f2343e1b7afd526582f606d68258ba3f0b6521a351e0ecb8bf3c52e with x1.
Apply Subq_atleastp with
Sing x1,
x0.
Let x2 of type ι be given.
Apply SingE with
x1,
x2,
λ x3 x4 . x4 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.