let X be set ; :: thesis: for B being Subset-Family of X st B = {X} holds
B is upper
let B be Subset-Family of X; :: thesis: ( B = {X} implies B is upper )
assume A1: B = {X} ; :: thesis: B is upper

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 A1, A3, TARSKI:def 1;
hence Y2 in B by A3; :: thesis: verum

end;

hence B is upper ; :: thesis: verum