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 P by XBOOLE_1:17;
field (LattRel L) = the carrier of L by FILTER_1:32;
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:13; :: according to XBOOLE_0:def 10 :: thesis: P c= field LR
let x be object ; :: 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:87;
then [x,x] in LR by XBOOLE_0:def 4;
hence x in field LR by RELAT_1:15; :: thesis: verum
end;
LR is reflexive by WELLORD1:15;
then A3: LR is_reflexive_in P by A2, RELAT_2:def 9;
then A4: dom LR = P by ORDERS_1:13;
LR is transitive by WELLORD1:17;
then A5: LR is_transitive_in P by A2, RELAT_2:def 16;
LR is antisymmetric by WELLORD1:18;
then A6: LR is_antisymmetric_in P by A2, RELAT_2:def 12;
reconsider LR = LR as Order of P by A4, PARTFUN1:def 2, WELLORD1:15, WELLORD1:17, WELLORD1:18;
set RS = RelStr(# P,LR #);
take IT = latt RelStr(# P,LR #); :: thesis: ( the carrier of IT = P & ( for x, y being Element of IT ex x9, y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) )
A7: RelStr(# P,LR #) is with_suprema
proof
let x, y be Element of RelStr(# P,LR #); :: according to LATTICE3:def 10 :: thesis: ex b1 being Element of the carrier of RelStr(# P,LR #) st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of RelStr(# P,LR #) holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
( x in P & y in P ) ;
then reconsider xL = x, yL = y as Element of L ;
consider zL being Element of L such that
A8: zL in P and
A9: xL [= zL and
A10: yL [= zL and
A11: for z9 being Element of L st z9 in P & xL [= z9 & yL [= z9 holds
zL [= z9 by Def6;
( [yL,zL] in [:P,P:] & [yL,zL] in LattRel L ) by A8, A10, FILTER_1:31, ZFMISC_1:87;
then A12: [yL,zL] in LR by XBOOLE_0:def 4;
reconsider z = zL as Element of RelStr(# P,LR #) by A8;
take z ; :: thesis: ( x <= z & y <= z & ( for b1 being Element of the carrier of RelStr(# P,LR #) holds
( not x <= b1 or not y <= b1 or z <= b1 ) ) )
( [xL,zL] in [:P,P:] & [xL,zL] in LattRel L ) by A8, A9, FILTER_1:31, ZFMISC_1:87;
then [xL,zL] in LR by XBOOLE_0:def 4;
hence ( x <= z & y <= z ) by A12, ORDERS_2:def 5; :: thesis: for b1 being Element of the carrier of RelStr(# P,LR #) holds
( not x <= b1 or not y <= b1 or z <= b1 )
let z9 be Element of RelStr(# P,LR #); :: thesis: ( not x <= z9 or not y <= z9 or z <= z9 )
assume that
A13: x <= z9 and
A14: y <= z9 ; :: thesis: z <= z9
z9 in P ;
then reconsider z9L = z9 as Element of L ;
[y,z9] in LR by A14, ORDERS_2:def 5;
then [y,z9] in LattRel L by XBOOLE_0:def 4;
then A15: yL [= z9L by FILTER_1:31;
[x,z9] in LR by A13, ORDERS_2:def 5;
then [x,z9] in LattRel L by XBOOLE_0:def 4;
then xL [= z9L by FILTER_1:31;
then zL [= z9L by A11, A15;
then A16: [zL,z9L] in LattRel L by FILTER_1:31;
[zL,z9L] in [:P,P:] by A8, ZFMISC_1:87;
then [zL,z9L] in LR by A16, XBOOLE_0:def 4;
hence z <= z9 by ORDERS_2:def 5; :: thesis: verum
end;
A17: RelStr(# P,LR #) is with_infima
proof
let x, y be Element of RelStr(# P,LR #); :: according to LATTICE3:def 11 :: thesis: ex b1 being Element of the carrier of RelStr(# P,LR #) st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of RelStr(# P,LR #) holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )
( x in P & y in P ) ;
then reconsider xL = x, yL = y as Element of L ;
consider zL being Element of L such that
A18: zL in P and
A19: zL [= xL and
A20: zL [= yL and
A21: for z9 being Element of L st z9 in P & z9 [= xL & z9 [= yL holds
z9 [= zL by Def7;
( [zL,yL] in [:P,P:] & [zL,yL] in LattRel L ) by A18, A20, FILTER_1:31, ZFMISC_1:87;
then A22: [zL,yL] in LR by XBOOLE_0:def 4;
reconsider z = zL as Element of RelStr(# P,LR #) by A18;
take z ; :: thesis: ( z <= x & z <= y & ( for b1 being Element of the carrier of RelStr(# P,LR #) holds
( not b1 <= x or not b1 <= y or b1 <= z ) ) )
( [zL,xL] in [:P,P:] & [zL,xL] in LattRel L ) by A18, A19, FILTER_1:31, ZFMISC_1:87;
then [zL,xL] in LR by XBOOLE_0:def 4;
hence ( z <= x & z <= y ) by A22, ORDERS_2:def 5; :: thesis: for b1 being Element of the carrier of RelStr(# P,LR #) holds
( not b1 <= x or not b1 <= y or b1 <= z )
let z9 be Element of RelStr(# P,LR #); :: thesis: ( not z9 <= x or not z9 <= y or z9 <= z )
assume that
A23: z9 <= x and
A24: z9 <= y ; :: thesis: z9 <= z
z9 in P ;
then reconsider z9L = z9 as Element of L ;
[z9,y] in LR by A24, ORDERS_2:def 5;
then [z9,y] in LattRel L by XBOOLE_0:def 4;
then A25: z9L [= yL by FILTER_1:31;
[z9,x] in LR by A23, ORDERS_2:def 5;
then [z9,x] in LattRel L by XBOOLE_0:def 4;
then z9L [= xL by FILTER_1:31;
then z9L [= zL by A21, A25;
then A26: [z9L,zL] in LattRel L by FILTER_1:31;
[z9L,zL] in [:P,P:] by A18, ZFMISC_1:87;
then [z9L,zL] in LR by A26, XBOOLE_0:def 4;
hence z9 <= z by ORDERS_2:def 5; :: thesis: verum
end;
A27: RelStr(# P,LR #) is Poset by A3, A6, A5, ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4;
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 IT ex x9, y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) )
let x, y be Element of IT; :: thesis: ex x9, y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) )
( x in P & y in P ) by A28;
then reconsider x9 = x, y9 = y as Element of L ;
take x9 ; :: thesis: ex y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) )
take y9 ; :: thesis: ( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) )
thus ( x = x9 & y = y9 ) ; :: thesis: ( ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) )
hereby :: thesis: ( x9 [= y9 implies x [= y )
assume x [= y ; :: thesis: x9 [= y9
then [x,y] in LR by A28, FILTER_1:31;
then [x,y] in LattRel L by XBOOLE_0:def 4;
hence x9 [= y9 by FILTER_1:31; :: thesis: verum
end;
assume x9 [= y9 ; :: thesis: x [= y
then A29: [x,y] in LattRel L by FILTER_1:31;
[x,y] in [:P,P:] by A28, ZFMISC_1:87;
then [x,y] in LattRel IT by A28, A29, XBOOLE_0:def 4;
hence x [= y by FILTER_1:31; :: thesis: verum