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

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

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 ) )

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

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

LR is reflexive
by WELLORD1:15;
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;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

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

A17:
RelStr(# P,LR #) is with_infima
let x, y be Element of RelStr(# P,LR #); :: according to LATTICE3:def 10 :: thesis: ex b_{1} being Element of the carrier of RelStr(# P,LR #) st

( x <= b_{1} & y <= b_{1} & ( for b_{2} being Element of the carrier of RelStr(# P,LR #) holds

( not x <= b_{2} or not y <= b_{2} or b_{1} <= b_{2} ) ) )

( 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 b_{1} being Element of the carrier of RelStr(# P,LR #) holds

( not x <= b_{1} or not y <= b_{1} or z <= b_{1} ) ) )

( [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 b_{1} being Element of the carrier of RelStr(# P,LR #) holds

( not x <= b_{1} or not y <= b_{1} or z <= b_{1} )

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;( x <= b

( not x <= b

( 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 b

( not x <= b

( [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 b

( not x <= b

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

proof

A27:
RelStr(# P,LR #) is Poset
by A3, A6, A5, ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4;
let x, y be Element of RelStr(# P,LR #); :: according to LATTICE3:def 11 :: thesis: ex b_{1} being Element of the carrier of RelStr(# P,LR #) st

( b_{1} <= x & b_{1} <= y & ( for b_{2} being Element of the carrier of RelStr(# P,LR #) holds

( not b_{2} <= x or not b_{2} <= y or b_{2} <= b_{1} ) ) )

( 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 b_{1} being Element of the carrier of RelStr(# P,LR #) holds

( not b_{1} <= x or not b_{1} <= y or b_{1} <= 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 b_{1} being Element of the carrier of RelStr(# P,LR #) holds

( not b_{1} <= x or not b_{1} <= y or b_{1} <= 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;( b

( not b

( 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 b

( not b

( [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 b

( not b

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

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
x9 [= y9
; :: thesis: x [= yassume
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;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

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