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;

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

( 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 A5:
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;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

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