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

( ( 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} )

( ( 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

hence
{X} is non empty Subset-Family of X
; :: thesis: ( not {} in {X} & ( for Y1, Y2 being Subset of X holds
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;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

( ( 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

thus
( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} )
:: thesis: verum
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;then ( Y1 = X & Y2 = X ) by TARSKI:def 1;

hence Y1 /\ Y2 in {X} by TARSKI:def 1; :: thesis: verum