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
A1: the carrier of (BoolePoset X) = bool X by LATTICE3:def 1;
reconsider Y' = Y as Subset of (BoolePoset X) by LATTICE3:def 1;
reconsider In = the InternalRel of (BoolePoset X) as Relation of (bool X) by A1;
for x being set st x in bool X holds
ex y being set st [x,y] in In

proof

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

end;

then A2: dom In = bool X by RELSET_1:22;
for y being set st y in bool X holds
ex x being set st [x,y] in In

proof

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

end;

then A3: field the InternalRel of (BoolePoset X) = (bool X) \/ (bool X) by A2, RELSET_1:23;

now

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 Y' = Y, Z' = 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 Y' <= Z' by ORDERS_2:def 9;
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 Y' <= Z' by Th2;
hence [Y,Z] in the InternalRel of (BoolePoset X) by ORDERS_2:def 9; :: thesis: verum

end;

end;

then A4: the InternalRel of (BoolePoset X) = RelIncl (bool X) by A3, WELLORD2:def 1;
RelStr(# Y',(the InternalRel of (BoolePoset X) |_2 Y') #) is full SubRelStr of BoolePoset X by YELLOW_0:57;
hence InclPoset Y is full SubRelStr of BoolePoset X by A4, WELLORD2:8; :: thesis: verum