now :: thesis: for x, y being set st x in {X} & y in {X} holds
x /\ y in {X}
let x, y be set ; :: thesis: ( x in {X} & y in {X} implies x /\ y in {X} )
assume that
A1: x in {X} and
A2: y in {X} ; :: thesis: x /\ y in {X}
( x = X & y = X ) by A1, A2, TARSKI:def 1;
hence x /\ y in {X} by TARSKI:def 1; :: thesis: verum
end;
then {X} is cap-closed ;
then reconsider B = {X} as non empty cap-closed Subset-Family of X by CARD_FIL:2;
now :: thesis: for Y1, Y2 being Subset of X st Y1 in B & Y1 c= Y2 holds
Y2 in B
let Y1, Y2 be Subset of X; :: thesis: ( Y1 in B & Y1 c= Y2 implies Y2 in B )
assume A3: ( Y1 in B & Y1 c= Y2 ) ; :: thesis: Y2 in B
( Y1 = X & Y2 = X ) by A3, TARSKI:def 1;
hence Y2 in B by A3; :: thesis: verum
end;
then B is upper ;
hence ex b1 being non empty cap-closed upper Subset-Family of X st b1 is with_non-empty_elements ; :: thesis: verum