set R = LattRel L;
set S = OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #);
OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #), the L_join of OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #), the L_meet of OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #), the Compl of OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #) #) ;
then reconsider S = OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #) as CLatAugmentation of L by Def12;
for x, y being Element of S holds
( x <= y iff x |^| y = x )
proof
let x, y be Element of S; :: thesis: ( x <= y iff x |^| y = x )
reconsider x9 = x, y9 = y as Element of L ;
hereby :: thesis: ( x |^| y = x implies x <= y )
assume x <= y ; :: thesis: x |^| y = x
then [x9,y9] in the InternalRel of S by ORDERS_2:def 5;
then x9 [= y9 by FILTER_1:31;
then x9 |^| y9 = x9 by LATTICES:4;
hence x |^| y = x ; :: thesis: verum
end;
A1: x9 |^| y9 = x |^| y ;
assume x |^| y = x ; :: thesis: x <= y
then x9 [= y9 by A1, LATTICES:4;
then [x9,y9] in LattRel L by FILTER_1:31;
hence x <= y by ORDERS_2:def 5; :: thesis: verum
end;
then A2: S is naturally_inf-generated ;
for x, y being Element of S holds
( x <= y iff x |_| y = y )
proof
let x, y be Element of S; :: thesis: ( x <= y iff x |_| y = y )
reconsider x9 = x, y9 = y as Element of L ;
hereby :: thesis: ( x |_| y = y implies x <= y )
assume x <= y ; :: thesis: x |_| y = y
then [x,y] in the InternalRel of S by ORDERS_2:def 5;
then x9 [= y9 by FILTER_1:31;
then x9 |_| y9 = y9 ;
hence x |_| y = y ; :: thesis: verum
end;
assume x |_| y = y ; :: thesis: x <= y
then x9 [= y9 ;
then [x9,y9] in LattRel L by FILTER_1:31;
hence x <= y by ORDERS_2:def 5; :: thesis: verum
end;
then S is naturally_sup-generated ;
hence ex b1 being CLatAugmentation of L st
( b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like ) by A2; :: thesis: verum