let X be set ; :: thesis: for Y being Subset of (BoolePoset X) 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 (BoolePoset X); :: 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 (BoolePoset X) = 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 (BoolePoset X) by A4, A5, Th2;
a <= b by A3, YELLOW_1:2;
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 (BoolePoset X); :: 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 A8, YELLOW_1:2;
hence b in Y by A1, A6, A7; :: thesis: verum