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 Th4;

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 A3: ( x c= y & y in Y ) ; :: thesis: x in Y
then reconsider a = x, b = y as Element of (BoolePoset X) by A1, XBOOLE_1:1;
a <= b by A3, YELLOW_1:2;
hence x in Y by A2, A3, WAYBEL_0:def 19; :: thesis: verum

end;

assume A4: 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 A5: ( a in Y & b <= a ) ; :: thesis: b in Y
then b c= a by YELLOW_1:2;
hence b in Y by A4, A5; :: thesis: verum