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

proof

let x, y be set ; :: 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 x' = x, y' = y as Element of L by ZFMISC_1:106;
x' <= y' by A2, ORDERS_2:def 9;
then x' [= y' by Th22;
hence [x,y] in LattRel L by FILTER_1:32; :: thesis: verum

end;

assume A3: [x,y] in LattRel L ; :: thesis: [x,y] in the InternalRel of L
then reconsider x' = x, y' = y as Element of L by ZFMISC_1:106;
x' [= y' by A3, FILTER_1:32;
then x' <= y' by Th22;
hence [x,y] in the InternalRel of L by ORDERS_2:def 9; :: thesis: verum

end;

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