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