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₁[ 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₁[x,y,u]

proof

let x, y be Element of A; :: thesis: ex u being Element of A st S₁[x,y,u]
reconsider x9 = x, y9 = y as Element of A ;
take x9 "\/" y9 ; :: thesis: S₁[x,y,x9 "\/" y9]
thus S₁[x,y,x9 "\/" y9] ; :: thesis: verum

end;

consider j being BinOp of the carrier of A such that
A2: for x, y being Element of A holds S₁[x,y,j . (x,y)] from BINOP_1:sch 3(A1);
defpred S₂[ 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₂[x,y,u]

proof

let x, y be Element of A; :: thesis: ex u being Element of A st S₂[x,y,u]
reconsider x9 = x, y9 = y as Element of A ;
take x9 "/\" y9 ; :: thesis: S₂[x,y,x9 "/\" y9]
thus S₂[x,y,x9 "/\" y9] ; :: thesis: verum

end;

consider m being BinOp of the carrier of A such that
A4: for x, y being Element of A holds S₂[x,y,m . (x,y)] from BINOP_1:sch 3(A3);
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;

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;

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;

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;

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;

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

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;

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

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 )

proof

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;

assume A13: [x,y] in the InternalRel of A ; :: thesis: [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;

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