let X be set ; :: thesis: for Y being Subset of () holds
( Y is upper iff for x, y being set st x c= y & y c= X & x in Y holds
y in Y )

let Y be Subset of (); :: thesis: ( Y is upper iff for x, y being set st x c= y & y c= X & x in Y holds
y in Y )

A1: the carrier of () = bool X by Th2;
hereby :: thesis: ( ( for x, y being set st x c= y & y c= X & x in Y holds
y in Y ) implies Y is upper )
assume A2: Y is upper ; :: thesis: for x, y being set st x c= y & y c= X & x in Y holds
y in Y

let x, y be set ; :: thesis: ( x c= y & y c= X & x in Y implies y in Y )
assume that
A3: x c= y and
A4: y c= X and
A5: x in Y ; :: thesis: y in Y
reconsider a = x, b = y as Element of () by A4, A5, Th2;
a <= b by ;
hence y in Y by A2, A5; :: thesis: verum
end;
assume A6: for x, y being set st x c= y & y c= X & x in Y holds
y in Y ; :: thesis: Y is upper
let a, b be Element of (); :: according to WAYBEL_0:def 20 :: thesis: ( not a in Y or not a <= b or b in Y )
assume that
A7: a in Y and
A8: b >= a ; :: thesis: b in Y
a c= b by ;
hence b in Y by A1, A6, A7; :: thesis: verum