let X be set ; :: thesis:
let x, y be Element of (BoolePoset X); :: thesis:
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:

assume A2: x << y ; :: thesis:
let Y be Subset-Family of X; :: thesis:
reconsider Y9 = Y as Subset of (BoolePoset X) by A1;
assume y c= union Y ; :: thesis:
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= sup Z by A4, YELLOW_1:2;
hence x c= union Z9 by YELLOW_1:21; :: thesis:

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:

end;

end;