let X be set ; :: thesis: for x, y being Element of (BoolePoset X) holds
( x << y iff for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z )
let x, y be Element of (BoolePoset X); :: thesis: ( x << y iff for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z )
LattPOSet (BooleLatt X) = RelStr(# the carrier of (BooleLatt X),(LattRel (BooleLatt X)) #) by LATTICE3:def 2;
then A1: the carrier of (BoolePoset X) = the carrier of (BooleLatt X) by YELLOW_1:def 2
.= bool X by LATTICE3:def 1 ;
thus ( x << y implies for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z ) :: thesis: ( ( for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z ) implies x << y )

proof

assume A2: x << y ; :: thesis: for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z
let Y be Subset-Family of X; :: thesis: ( y c= union Y implies ex Z being finite Subset of Y st x c= union Z )
reconsider Y' = Y as Subset of (BoolePoset X) by A1;
assume y c= union Y ; :: thesis: ex Z being finite Subset of Y st x c= union Z
then y c= sup Y' by YELLOW_1:21;
then y <= sup Y' by YELLOW_1:2;
then consider Z being finite Subset of (BoolePoset X) such that
A3: ( Z c= Y & x <= sup Z ) by A2, WAYBEL_3:18;
reconsider Z' = Z as finite Subset of Y by A3;
take Z' ; :: thesis: x c= union Z'
x c= sup Z by A3, YELLOW_1:2;
hence x c= union Z' by YELLOW_1:21; :: thesis: verum

end;

thus ( ( for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z ) implies x << y ) :: thesis: verum

proof

assume A4: for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z ; :: thesis: x << y

now

let Y be Subset of (BoolePoset X); :: thesis: ( y <= sup Y implies ex Z being finite Subset of (BoolePoset X) st
( Z c= Y & x <= sup Z ) )
reconsider Y' = Y as Subset-Family of X by A1;
assume y <= sup Y ; :: thesis: ex Z being finite Subset of (BoolePoset X) st
( Z c= Y & x <= sup Z )
then y c= sup Y by YELLOW_1:2;
then y c= union Y' by YELLOW_1:21;
then consider Z' being finite Subset of Y' such that
A5: x c= union Z' by A4;
reconsider Z = Z' as finite Subset of (BoolePoset X) by XBOOLE_1:1;
take Z = Z; :: thesis: ( Z c= Y & x <= sup Z )
thus Z c= Y ; :: thesis: x <= sup Z
x c= sup Z by A5, YELLOW_1:21;
hence x <= sup Z by YELLOW_1:2; :: thesis: verum

end;

hence x << y by WAYBEL_3:19; :: thesis: verum

end;