let A be with_suprema with_infima Poset; :: thesis: ex L being strict Lattice st RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet L

defpred S_{1}[ Element of A, Element of A, set ] means for x9, y9 being Element of A st x9 = $1 & y9 = $2 holds

$3 = x9 "\/" y9;

A1: for x, y being Element of A ex u being Element of A st S_{1}[x,y,u]

A2: for x, y being Element of A holds S_{1}[x,y,j . (x,y)]
from BINOP_1:sch 3(A1);

defpred S_{2}[ Element of A, Element of A, set ] means for x9, y9 being Element of A st x9 = $1 & y9 = $2 holds

$3 = x9 "/\" y9;

A3: for x, y being Element of A ex u being Element of A st S_{2}[x,y,u]

A4: for x, y being Element of A holds S_{2}[x,y,m . (x,y)]
from BINOP_1:sch 3(A3);

set L = LattStr(# the carrier of A,j,m #);

then reconsider L = LattStr(# the carrier of A,j,m #) as strict Lattice ;

take L ; :: thesis: RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet L

A10: LattRel L = { [p,q] where p, q is Element of L : p [= q } by FILTER_1:def 8;

LattRel L = the InternalRel of A

defpred S

$3 = x9 "\/" y9;

A1: for x, y being Element of A ex u being Element of A st S

proof

consider j being BinOp of the carrier of A such that
let x, y be Element of A; :: thesis: ex u being Element of A st S_{1}[x,y,u]

reconsider x9 = x, y9 = y as Element of A ;

take x9 "\/" y9 ; :: thesis: S_{1}[x,y,x9 "\/" y9]

thus S_{1}[x,y,x9 "\/" y9]
; :: thesis: verum

end;reconsider x9 = x, y9 = y as Element of A ;

take x9 "\/" y9 ; :: thesis: S

thus S

A2: for x, y being Element of A holds S

defpred S

$3 = x9 "/\" y9;

A3: for x, y being Element of A ex u being Element of A st S

proof

consider m being BinOp of the carrier of A such that
let x, y be Element of A; :: thesis: ex u being Element of A st S_{2}[x,y,u]

reconsider x9 = x, y9 = y as Element of A ;

take x9 "/\" y9 ; :: thesis: S_{2}[x,y,x9 "/\" y9]

thus S_{2}[x,y,x9 "/\" y9]
; :: thesis: verum

end;reconsider x9 = x, y9 = y as Element of A ;

take x9 "/\" y9 ; :: thesis: S

thus S

A4: for x, y being Element of A holds S

set L = LattStr(# the carrier of A,j,m #);

A5: now :: thesis: for a, b being Element of LattStr(# the carrier of A,j,m #) holds a "\/" b = b "\/" a

let a, b be Element of LattStr(# the carrier of A,j,m #); :: thesis: a "\/" b = b "\/" a

reconsider x = a, y = b as Element of A ;

j . (x,y) = x "\/" y by A2;

hence a "\/" b = b "\/" a by A2; :: thesis: verum

end;reconsider x = a, y = b as Element of A ;

j . (x,y) = x "\/" y by A2;

hence a "\/" b = b "\/" a by A2; :: thesis: verum

A6: now :: thesis: for a, b, c being Element of LattStr(# the carrier of A,j,m #) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c

let a, b, c be Element of LattStr(# the carrier of A,j,m #); :: thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c

reconsider x = a, y = b, z = c as Element of A ;

thus a "\/" (b "\/" c) = j . (x,(y "\/" z)) by A2

.= x "\/" (y "\/" z) by A2

.= (x "\/" y) "\/" z by Th14

.= j . ((x "\/" y),z) by A2

.= (a "\/" b) "\/" c by A2 ; :: thesis: verum

end;reconsider x = a, y = b, z = c as Element of A ;

thus a "\/" (b "\/" c) = j . (x,(y "\/" z)) by A2

.= x "\/" (y "\/" z) by A2

.= (x "\/" y) "\/" z by Th14

.= j . ((x "\/" y),z) by A2

.= (a "\/" b) "\/" c by A2 ; :: thesis: verum

A7: now :: thesis: for a, b being Element of LattStr(# the carrier of A,j,m #) holds (a "/\" b) "\/" b = b

let a, b be Element of LattStr(# the carrier of A,j,m #); :: thesis: (a "/\" b) "\/" b = b

reconsider x = a, y = b as Element of A ;

thus (a "/\" b) "\/" b = j . ((x "/\" y),y) by A4

.= (x "/\" y) "\/" y by A2

.= b by Th17 ; :: thesis: verum

end;reconsider x = a, y = b as Element of A ;

thus (a "/\" b) "\/" b = j . ((x "/\" y),y) by A4

.= (x "/\" y) "\/" y by A2

.= b by Th17 ; :: thesis: verum

A8: now :: thesis: for a, b being Element of LattStr(# the carrier of A,j,m #) holds a "/\" b = b "/\" a

let a, b be Element of LattStr(# the carrier of A,j,m #); :: thesis: a "/\" b = b "/\" a

reconsider x = a, y = b as Element of A ;

m . (x,y) = x "/\" y by A4;

hence a "/\" b = b "/\" a by A4; :: thesis: verum

end;reconsider x = a, y = b as Element of A ;

m . (x,y) = x "/\" y by A4;

hence a "/\" b = b "/\" a by A4; :: thesis: verum

A9: now :: thesis: for a, b, c being Element of LattStr(# the carrier of A,j,m #) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c

let a, b, c be Element of LattStr(# the carrier of A,j,m #); :: thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c

reconsider x = a, y = b, z = c as Element of A ;

thus a "/\" (b "/\" c) = m . (x,(y "/\" z)) by A4

.= x "/\" (y "/\" z) by A4

.= (x "/\" y) "/\" z by Th16

.= m . ((x "/\" y),z) by A4

.= (a "/\" b) "/\" c by A4 ; :: thesis: verum

end;reconsider x = a, y = b, z = c as Element of A ;

thus a "/\" (b "/\" c) = m . (x,(y "/\" z)) by A4

.= x "/\" (y "/\" z) by A4

.= (x "/\" y) "/\" z by Th16

.= m . ((x "/\" y),z) by A4

.= (a "/\" b) "/\" c by A4 ; :: thesis: verum

now :: thesis: for a, b being Element of LattStr(# the carrier of A,j,m #) holds a "/\" (a "\/" b) = a

then
( LattStr(# the carrier of A,j,m #) is join-commutative & LattStr(# the carrier of A,j,m #) is join-associative & LattStr(# the carrier of A,j,m #) is meet-absorbing & LattStr(# the carrier of A,j,m #) is meet-commutative & LattStr(# the carrier of A,j,m #) is meet-associative & LattStr(# the carrier of A,j,m #) is join-absorbing )
by A5, A6, A7, A8, A9;let a, b be Element of LattStr(# the carrier of A,j,m #); :: thesis: a "/\" (a "\/" b) = a

reconsider x = a, y = b as Element of A ;

thus a "/\" (a "\/" b) = m . (x,(x "\/" y)) by A2

.= x "/\" (x "\/" y) by A4

.= a by Th18 ; :: thesis: verum

end;reconsider x = a, y = b as Element of A ;

thus a "/\" (a "\/" b) = m . (x,(x "\/" y)) by A2

.= x "/\" (x "\/" y) by A4

.= a by Th18 ; :: thesis: verum

then reconsider L = LattStr(# the carrier of A,j,m #) as strict Lattice ;

take L ; :: thesis: RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet L

A10: LattRel L = { [p,q] where p, q is Element of L : p [= q } by FILTER_1:def 8;

LattRel L = the InternalRel of A

proof

hence
RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet L
; :: thesis: verum
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in LattRel L or [x,y] in the InternalRel of A ) & ( not [x,y] in the InternalRel of A or [x,y] in LattRel L ) )

thus ( [x,y] in LattRel L implies [x,y] in the InternalRel of A ) :: thesis: ( not [x,y] in the InternalRel of A or [x,y] in LattRel L )

then consider x1, x2 being object such that

A14: x1 in the carrier of A and

A15: x2 in the carrier of A and

A16: [x,y] = [x1,x2] by ZFMISC_1:84;

reconsider x1 = x1, x2 = x2 as Element of A by A14, A15;

reconsider y1 = x1, y2 = x2 as Element of L ;

A17: x1 <= x2 by A13, A16;

x2 <= x2 ;

then A18: x1 "\/" x2 <= x2 by A17, Lm1;

x2 <= x1 "\/" x2 by Lm1;

then x2 = x1 "\/" x2 by A18, ORDERS_2:2

.= y1 "\/" y2 by A2 ;

then y1 [= y2 ;

hence [x,y] in LattRel L by A10, A16; :: thesis: verum

end;thus ( [x,y] in LattRel L implies [x,y] in the InternalRel of A ) :: thesis: ( not [x,y] in the InternalRel of A or [x,y] in LattRel L )

proof

assume A13:
[x,y] in the InternalRel of A
; :: thesis: [x,y] in LattRel L
assume
[x,y] in LattRel L
; :: thesis: [x,y] in the InternalRel of A

then consider p, q being Element of L such that

A11: [x,y] = [p,q] and

A12: p [= q by A10;

reconsider p9 = p, q9 = q as Element of A ;

p9 "\/" q9 = p "\/" q by A2

.= q by A12 ;

then p9 <= q9 by Lm1;

hence [x,y] in the InternalRel of A by A11; :: thesis: verum

end;then consider p, q being Element of L such that

A11: [x,y] = [p,q] and

A12: p [= q by A10;

reconsider p9 = p, q9 = q as Element of A ;

p9 "\/" q9 = p "\/" q by A2

.= q by A12 ;

then p9 <= q9 by Lm1;

hence [x,y] in the InternalRel of A by A11; :: thesis: verum

then consider x1, x2 being object such that

A14: x1 in the carrier of A and

A15: x2 in the carrier of A and

A16: [x,y] = [x1,x2] by ZFMISC_1:84;

reconsider x1 = x1, x2 = x2 as Element of A by A14, A15;

reconsider y1 = x1, y2 = x2 as Element of L ;

A17: x1 <= x2 by A13, A16;

x2 <= x2 ;

then A18: x1 "\/" x2 <= x2 by A17, Lm1;

x2 <= x1 "\/" x2 by Lm1;

then x2 = x1 "\/" x2 by A18, ORDERS_2:2

.= y1 "\/" y2 by A2 ;

then y1 [= y2 ;

hence [x,y] in LattRel L by A10, A16; :: thesis: verum