let L be non empty Lattice-like naturally_sup-generated LattRelStr ; :: thesis: RelStr(# the carrier of L, the InternalRel of L #) = LattPOSet L
A1: for x, y being object holds
( [x,y] in the InternalRel of L iff [x,y] in LattRel L )

proof

let x, y be object ; :: thesis: ( [x,y] in the InternalRel of L iff [x,y] in LattRel L )

hereby :: thesis: ( [x,y] in LattRel L implies [x,y] in the InternalRel of L )

assume A2: [x,y] in the InternalRel of L ; :: thesis: [x,y] in LattRel L
then reconsider x9 = x, y9 = y as Element of L by ZFMISC_1:87;
x9 <= y9 by A2, ORDERS_2:def 5;
then x9 [= y9 by Th22;
hence [x,y] in LattRel L by FILTER_1:31; :: thesis: verum

end;

assume A3: [x,y] in LattRel L ; :: thesis: [x,y] in the InternalRel of L
then reconsider x9 = x, y9 = y as Element of L by ZFMISC_1:87;
x9 [= y9 by A3, FILTER_1:31;
then x9 <= y9 by Th22;
hence [x,y] in the InternalRel of L by ORDERS_2:def 5; :: thesis: verum

end;

LattPOSet L = RelStr(# the carrier of L,(LattRel L) #) by LATTICE3:def 2;
hence RelStr(# the carrier of L, the InternalRel of L #) = LattPOSet L by A1, RELAT_1:def 2; :: thesis: verum