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;

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

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

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