let X be set ; :: thesis: for Y being Subset-Family of X holds InclPoset Y is full SubRelStr of BoolePoset X
set L = BoolePoset X;
let Y be Subset-Family of X; :: thesis: InclPoset Y is full SubRelStr of BoolePoset X
reconsider Y9 = Y as Subset of (BoolePoset X) by LATTICE3:def 1;
the carrier of (BoolePoset X) = bool X by LATTICE3:def 1;
then reconsider In = the InternalRel of (BoolePoset X) as Relation of (bool X) ;
for x being object st x in bool X holds
ex y being object st [x,y] in In

proof

let x be object ; :: thesis: ( x in bool X implies ex y being object st [x,y] in In )
assume x in bool X ; :: thesis: ex y being object st [x,y] in In
then reconsider x9 = x as Element of (BoolePoset X) by LATTICE3:def 1;
take y = x9; :: thesis: [x,y] in In
x9 <= y ;
hence [x,y] in In by ORDERS_2:def 5; :: thesis: verum

end;

then A1: dom In = bool X by RELSET_1:9;

A2: now :: thesis: for Y, Z being set st Y in bool X & Z in bool X holds
( ( [Y,Z] in the InternalRel of (BoolePoset X) implies Y c= Z ) & ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) ) )

let Y, Z be set ; :: thesis: ( Y in bool X & Z in bool X implies ( ( [Y,Z] in the InternalRel of (BoolePoset X) implies Y c= Z ) & ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) ) ) )
assume ( Y in bool X & Z in bool X ) ; :: thesis: ( ( [Y,Z] in the InternalRel of (BoolePoset X) implies Y c= Z ) & ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) ) )
then reconsider Y9 = Y, Z9 = Z as Element of (BoolePoset X) by LATTICE3:def 1;
thus ( [Y,Z] in the InternalRel of (BoolePoset X) implies Y c= Z ) :: thesis: ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) )

proof

assume [Y,Z] in the InternalRel of (BoolePoset X) ; :: thesis: Y c= Z
then Y9 <= Z9 by ORDERS_2:def 5;
hence Y c= Z by Th2; :: thesis: verum

end;

thus ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) ) :: thesis: verum

proof

assume Y c= Z ; :: thesis: [Y,Z] in the InternalRel of (BoolePoset X)
then Y9 <= Z9 by Th2;
hence [Y,Z] in the InternalRel of (BoolePoset X) by ORDERS_2:def 5; :: thesis: verum

end;

end;

for y being object st y in bool X holds
ex x being object st [x,y] in In

proof

let y be object ; :: thesis: ( y in bool X implies ex x being object st [x,y] in In )
assume y in bool X ; :: thesis: ex x being object st [x,y] in In
then reconsider y9 = y as Element of (BoolePoset X) by LATTICE3:def 1;
take x = y9; :: thesis: [x,y] in In
x <= y9 ;
hence [x,y] in In by ORDERS_2:def 5; :: thesis: verum

end;

then field the InternalRel of (BoolePoset X) = (bool X) \/ (bool X) by A1, RELSET_1:10;
then A3: the InternalRel of (BoolePoset X) = RelIncl (bool X) by A2, WELLORD2:def 1;
RelStr(# Y9,( the InternalRel of (BoolePoset X) |_2 Y9) #) is full SubRelStr of BoolePoset X by YELLOW_0:56;
hence InclPoset Y is full SubRelStr of BoolePoset X by A3, WELLORD2:7; :: thesis: verum