take
{X}
; :: thesis: ( {X} is non empty Subset-Family of X & not {} in {X} & ( for Y1, Y2 being Subset of X holds

( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ) ) )

thus ( {X} is non empty Subset-Family of X & not {} in {X} & ( for Y1, Y2 being Subset of X holds

( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ) ) ) by Th2; :: thesis: verum

( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ) ) )

thus ( {X} is non empty Subset-Family of X & not {} in {X} & ( for Y1, Y2 being Subset of X holds

( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ) ) ) by Th2; :: thesis: verum