let X be set ; :: thesis: for Y being Subset of (BoolePoset X) holds
( Y is lower iff for x, y being set st x c= y & y in Y holds
x in Y )
let Y be Subset of (BoolePoset X); :: thesis: ( Y is lower iff for x, y being set st x c= y & y in Y holds
x in Y )
A1: the carrier of (BoolePoset X) = bool X by Th2;

hereby :: thesis: ( ( for x, y being set st x c= y & y in Y holds
x in Y ) implies Y is lower )

assume A2: Y is lower ; :: thesis: for x, y being set st x c= y & y in Y holds
x in Y
let x, y be set ; :: thesis: ( x c= y & y in Y implies x in Y )
assume that
A3: x c= y and
A4: y in Y ; :: thesis: x in Y
reconsider a = x, b = y as Element of (BoolePoset X) by A1, A3, A4, XBOOLE_1:1;
a <= b by A3, YELLOW_1:2;
hence x in Y by A2, A4; :: thesis: verum

end;

assume A5: for x, y being set st x c= y & y in Y holds
x in Y ; :: thesis: Y is lower
let a, b be Element of (BoolePoset X); :: according to WAYBEL_0:def 19 :: thesis: ( not a in Y or not b <= a or b in Y )
assume that
A6: a in Y and
A7: b <= a ; :: thesis: b in Y
b c= a by A7, YELLOW_1:2;
hence b in Y by A5, A6; :: thesis: verum