per cases ( not X is empty or X is empty ) ;

suppose not X is empty ; :: thesis: ex b₁ being non empty cap-closed Subset-Family of X st b₁ is upper

then reconsider B = {X} as non empty Subset-Family of X by CARD_FIL:2;

A1: 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 ( x in {X} & y in {X} ) ; :: thesis: x /\ y in {X}
then ( x = X & y = X ) by TARSKI:def 1;
hence x /\ y in {X} by TARSKI:def 1; :: thesis: verum

end;

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 A2: ( Y1 in B & Y1 c= Y2 ) ; :: thesis: Y2 in B
then ( Y1 = X & Y2 = X ) by TARSKI:def 1;
hence Y2 in B by A2; :: thesis: verum

end;

then ( B is cap-closed & B is upper ) by A1;
hence ex b₁ being non empty cap-closed Subset-Family of X st b₁ is upper ; :: thesis: verum

end;

suppose A3: X is empty ; :: thesis: ex b₁ being non empty cap-closed Subset-Family of X st b₁ is upper

now :: thesis: for x, y being set st x in {{}} & y in {{}} holds
x /\ y in {{}}

let x, y be set ; :: thesis: ( x in {{}} & y in {{}} implies x /\ y in {{}} )
assume ( x in {{}} & y in {{}} ) ; :: thesis: x /\ y in {{}}
then ( x = {} & y = {} ) by TARSKI:def 1;
hence x /\ y in {{}} by TARSKI:def 1; :: thesis: verum

end;

then {{}} is cap-closed ;
then reconsider B = {{}} as non empty cap-closed Subset-Family of {} by SETFAM_1:46;
B is upper ;
hence ex b₁ being non empty cap-closed Subset-Family of X st b₁ is upper by A3; :: thesis: verum

end;

end;