let X be set ; :: thesis: BoolePoset X = InclPoset (bool X)
set B = BoolePoset X;
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 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 A1: 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 A2: field the InternalRel of (BoolePoset X) = (bool X) \/ (bool X) by A1, 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 the InternalRel of (BoolePoset X) = RelIncl (bool X) by A2, WELLORD2:def 1;
hence BoolePoset X = InclPoset (bool X) by LATTICE3:def 1; :: thesis: verum