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 x', y' being Element of A st x' = $1 & y' = $2 holds
$3 = x' "\/" y';
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 x' = x, y' = y as Element of A ;
take x' "\/" y' ; :: thesis: S₁[x,y,x' "\/" y']
thus S₁[x,y,x' "\/" y'] ; :: 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 x', y' being Element of A st x' = $1 & y' = $2 holds
$3 = x' "/\" y';
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 x' = x, y' = y as Element of A ;
take x' "/\" y' ; :: thesis: S₂[x,y,x' "/\" y']
thus S₂[x,y,x' "/\" y'] ; :: 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

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 ;
( x "\/" y = y "\/" x & a "\/" b = j . a,b & b "\/" a = j . b,a & j . x,y = x "\/" y & j . y,x = y "\/" x ) by A2;
hence a "\/" b = b "\/" a ; :: thesis: verum

end;

A6: now

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

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

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 ;
( x "/\" y = y "/\" x & a "/\" b = m . a,b & b "/\" a = m . b,a & m . x,y = x "/\" y & m . y,x = y "/\" x ) by A4;
hence a "/\" b = b "/\" a ; :: thesis: verum

end;

A9: now

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

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, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
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 set ; :: 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] & p [= q ) by A10;
reconsider p' = p, q' = q as Element of A ;
p' "\/" q' = p "\/" q by A2
.= q by A11, LATTICES:def 3 ;
then p' <= q' by Lm1;
hence [x,y] in the InternalRel of A by A11, ORDERS_2:def 9; :: thesis: verum

end;

assume A12: [x,y] in the InternalRel of A ; :: thesis: [x,y] in LattRel L
then consider x1, x2 being set such that
A13: ( x1 in the carrier of A & x2 in the carrier of A & [x,y] = [x1,x2] ) by ZFMISC_1:103;
reconsider x1 = x1, x2 = x2 as Element of A by A13;
reconsider y1 = x1, y2 = x2 as Element of L ;
( x1 <= x2 & x2 <= x2 ) by A12, A13, ORDERS_2:def 9;
then ( x1 "\/" x2 <= x2 & x2 <= x1 "\/" x2 ) by Lm1;
then x2 = x1 "\/" x2 by ORDERS_2:25
.= y1 "\/" y2 by A2 ;
then y1 [= y2 by LATTICES:def 3;
hence [x,y] in LattRel L by A10, A13; :: thesis: verum

end;

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