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 Y9 = 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 Y9 by YELLOW_1:21;
then y <= sup Y9 by YELLOW_1:2;
then consider Z being finite Subset of (BoolePoset X) such that
A3: Z c= Y and
A4: x <= sup Z by A2, WAYBEL_3:18;
reconsider Z9 = Z as finite Subset of Y by A3;
take Z9 ; :: thesis: x c= union Z9
x c= sup Z by A4, YELLOW_1:2;
hence x c= union Z9 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 A5: 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 :: thesis: for Y being Subset of (BoolePoset X) st y <= sup Y holds
ex Z being finite Subset of (BoolePoset X) st
( Z c= Y & x <= sup Z )

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 Y9 = 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 Y9 by YELLOW_1:21;
then consider Z9 being finite Subset of Y9 such that
A6: x c= union Z9 by A5;
reconsider Z = Z9 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 A6, YELLOW_1:21;
hence x <= sup Z by YELLOW_1:2; :: thesis: verum

end;

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

end;