let X be non empty set ; :: 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} ) ) ) )
A1: X c= X ;
{X} c= bool X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {X} or x in bool X )
assume x in {X} ; :: thesis: x in bool X
then x = X by TARSKI:def 1;
hence x in bool X by A1; :: thesis: verum
end;
hence {X} is non empty Subset-Family of X ; :: thesis: ( 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 not {} in {X} by TARSKI:def 1; :: thesis: 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} ) )
let Y1, Y2 be Subset of X; :: thesis: ( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) )
thus ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) :: thesis: ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} )
proof
assume ( Y1 in {X} & Y2 in {X} ) ; :: thesis: Y1 /\ Y2 in {X}
then ( Y1 = X & Y2 = X ) by TARSKI:def 1;
hence Y1 /\ Y2 in {X} by TARSKI:def 1; :: thesis: verum
end;
thus ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) :: thesis: verum
proof
assume ( Y1 in {X} & Y1 c= Y2 ) ; :: thesis: Y2 in {X}
then X c= Y2 by TARSKI:def 1;
then Y2 = X ;
hence Y2 in {X} by TARSKI:def 1; :: thesis: verum
end;