set cL = the carrier of L;
set LL = LattRel L;
set LR = (LattRel L) |_2 P;
reconsider LR = (LattRel L) |_2 P as Relation of by XBOOLE_1:17;
field (LattRel L) = the carrier of L by FILTER_1:33;
then A1: LattRel L is_reflexive_in the carrier of L by RELAT_2:def 9;
A2: field LR = P

proof

thus field LR c= P by WELLORD1:20; :: according to XBOOLE_0:def 10 :: thesis: P c= field LR
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in field LR )
assume x in P ; :: thesis: x in field LR
then ( [x,x] in [:P,P:] & [x,x] in LattRel L ) by A1, RELAT_2:def 1, ZFMISC_1:106;
then [x,x] in LR by XBOOLE_0:def 4;
hence x in field LR by RELAT_1:30; :: thesis: verum

end;

LR is reflexive by WELLORD1:22;
then A3: LR is_reflexive_in P by A2, RELAT_2:def 9;
then A4: dom LR = P by ORDERS_1:98;
LR is transitive by WELLORD1:24;
then A5: LR is_transitive_in P by A2, RELAT_2:def 16;
LR is antisymmetric by WELLORD1:25;
then A6: LR is_antisymmetric_in P by A2, RELAT_2:def 12;
reconsider LR = LR as Order of by A4, PARTFUN1:def 4, WELLORD1:22, WELLORD1:24, WELLORD1:25;
set RS = RelStr(# P,LR #);
take IT = latt RelStr(# P,LR #); :: thesis: ( the carrier of IT = P & ( for x, y being Element of ex x', y' being Element of st
( x = x' & y = y' & ( x [= y implies x' [= y' ) & ( x' [= y' implies x [= y ) ) ) )
A7: RelStr(# P,LR #) is with_suprema

proof

let x, y be Element of ; :: according to LATTICE3:def 10 :: thesis: ex b₁ being Element of the carrier of RelStr(# P,LR #) st
( x <= b₁ & y <= b₁ & ( for b₂ being Element of the carrier of RelStr(# P,LR #) holds
( not x <= b₂ or not y <= b₂ or b₁ <= b₂ ) ) )
( x in P & y in P ) ;
then reconsider xL = x, yL = y as Element of ;
consider zL being Element of such that
A8: zL in P and
A9: xL [= zL and
A10: yL [= zL and
A11: for z' being Element of st z' in P & xL [= z' & yL [= z' holds
zL [= z' by Def8;
( [yL,zL] in [:P,P:] & [yL,zL] in LattRel L ) by A8, A10, FILTER_1:32, ZFMISC_1:106;
then A12: [yL,zL] in LR by XBOOLE_0:def 4;
reconsider z = zL as Element of by A8;
take z ; :: thesis: ( x <= z & y <= z & ( for b₁ being Element of the carrier of RelStr(# P,LR #) holds
( not x <= b₁ or not y <= b₁ or z <= b₁ ) ) )
( [xL,zL] in [:P,P:] & [xL,zL] in LattRel L ) by A8, A9, FILTER_1:32, ZFMISC_1:106;
then [xL,zL] in LR by XBOOLE_0:def 4;
hence ( x <= z & y <= z ) by A12, ORDERS_2:def 9; :: thesis: for b₁ being Element of the carrier of RelStr(# P,LR #) holds
( not x <= b₁ or not y <= b₁ or z <= b₁ )
let z' be Element of ; :: thesis: ( not x <= z' or not y <= z' or z <= z' )
assume that
A13: x <= z' and
A14: y <= z' ; :: thesis: z <= z'
z' in P ;
then reconsider z'L = z' as Element of ;
[y,z'] in LR by A14, ORDERS_2:def 9;
then [y,z'] in LattRel L by XBOOLE_0:def 4;
then A15: yL [= z'L by FILTER_1:32;
[x,z'] in LR by A13, ORDERS_2:def 9;
then [x,z'] in LattRel L by XBOOLE_0:def 4;
then xL [= z'L by FILTER_1:32;
then zL [= z'L by A11, A15;
then A16: [zL,z'L] in LattRel L by FILTER_1:32;
[zL,z'L] in [:P,P:] by A8, ZFMISC_1:106;
then [zL,z'L] in LR by A16, XBOOLE_0:def 4;
hence z <= z' by ORDERS_2:def 9; :: thesis: verum

end;

A17: RelStr(# P,LR #) is with_infima

proof

let x, y be Element of ; :: according to LATTICE3:def 11 :: thesis: ex b₁ being Element of the carrier of RelStr(# P,LR #) st
( b₁ <= x & b₁ <= y & ( for b₂ being Element of the carrier of RelStr(# P,LR #) holds
( not b₂ <= x or not b₂ <= y or b₂ <= b₁ ) ) )
( x in P & y in P ) ;
then reconsider xL = x, yL = y as Element of ;
consider zL being Element of such that
A18: zL in P and
A19: zL [= xL and
A20: zL [= yL and
A21: for z' being Element of st z' in P & z' [= xL & z' [= yL holds
z' [= zL by Def9;
( [zL,yL] in [:P,P:] & [zL,yL] in LattRel L ) by A18, A20, FILTER_1:32, ZFMISC_1:106;
then A22: [zL,yL] in LR by XBOOLE_0:def 4;
reconsider z = zL as Element of by A18;
take z ; :: thesis: ( z <= x & z <= y & ( for b₁ being Element of the carrier of RelStr(# P,LR #) holds
( not b₁ <= x or not b₁ <= y or b₁ <= z ) ) )
( [zL,xL] in [:P,P:] & [zL,xL] in LattRel L ) by A18, A19, FILTER_1:32, ZFMISC_1:106;
then [zL,xL] in LR by XBOOLE_0:def 4;
hence ( z <= x & z <= y ) by A22, ORDERS_2:def 9; :: thesis: for b₁ being Element of the carrier of RelStr(# P,LR #) holds
( not b₁ <= x or not b₁ <= y or b₁ <= z )
let z' be Element of ; :: thesis: ( not z' <= x or not z' <= y or z' <= z )
assume that
A23: z' <= x and
A24: z' <= y ; :: thesis: z' <= z
z' in P ;
then reconsider z'L = z' as Element of ;
[z',y] in LR by A24, ORDERS_2:def 9;
then [z',y] in LattRel L by XBOOLE_0:def 4;
then A25: z'L [= yL by FILTER_1:32;
[z',x] in LR by A23, ORDERS_2:def 9;
then [z',x] in LattRel L by XBOOLE_0:def 4;
then z'L [= xL by FILTER_1:32;
then z'L [= zL by A21, A25;
then A26: [z'L,zL] in LattRel L by FILTER_1:32;
[z'L,zL] in [:P,P:] by A18, ZFMISC_1:106;
then [z'L,zL] in LR by A26, XBOOLE_0:def 4;
hence z' <= z by ORDERS_2:def 9; :: thesis: verum

end;

A27: RelStr(# P,LR #) is Poset by A3, A6, A5, ORDERS_2:def 4, ORDERS_2:def 5, ORDERS_2:def 6;
then A28: RelStr(# P,LR #) = LattPOSet IT by A7, A17, LATTICE3:def 15;
LattPOSet IT = RelStr(# the carrier of IT,(LattRel IT) #) ;
hence the carrier of IT = P by A7, A17, A27, LATTICE3:def 15; :: thesis: for x, y being Element of ex x', y' being Element of st
( x = x' & y = y' & ( x [= y implies x' [= y' ) & ( x' [= y' implies x [= y ) )
let x, y be Element of ; :: thesis: ex x', y' being Element of st
( x = x' & y = y' & ( x [= y implies x' [= y' ) & ( x' [= y' implies x [= y ) )
( x in P & y in P ) by A28;
then reconsider x' = x, y' = y as Element of ;
take x' ; :: thesis: ex y' being Element of st
( x = x' & y = y' & ( x [= y implies x' [= y' ) & ( x' [= y' implies x [= y ) )
take y' ; :: thesis: ( x = x' & y = y' & ( x [= y implies x' [= y' ) & ( x' [= y' implies x [= y ) )
thus ( x = x' & y = y' ) ; :: thesis: ( ( x [= y implies x' [= y' ) & ( x' [= y' implies x [= y ) )

hereby :: thesis: ( x' [= y' implies x [= y )

assume x [= y ; :: thesis: x' [= y'
then [x,y] in LR by A28, FILTER_1:32;
then [x,y] in LattRel L by XBOOLE_0:def 4;
hence x' [= y' by FILTER_1:32; :: thesis: verum

end;

assume x' [= y' ; :: thesis: x [= y
then A29: [x,y] in LattRel L by FILTER_1:32;
[x,y] in [:P,P:] by A28, ZFMISC_1:106;
then [x,y] in LattRel IT by A28, A29, XBOOLE_0:def 4;
hence x [= y by FILTER_1:32; :: thesis: verum