deffunc H1( Element of SubstitutionSet (V,C), Element of SubstitutionSet (V,C)) -> Element of SubstitutionSet (V,C) = mi ($1 \/ $2);
consider j being BinOp of (SubstitutionSet (V,C)) such that
A1:
for x, y being Element of SubstitutionSet (V,C) holds j . (x,y) = H1(x,y)
from BINOP_1:sch 4();
deffunc H2( Element of SubstitutionSet (V,C), Element of SubstitutionSet (V,C)) -> Element of SubstitutionSet (V,C) = mi ($1 ^ $2);
consider m being BinOp of (SubstitutionSet (V,C)) such that
A2:
for x, y being Element of SubstitutionSet (V,C) holds m . (x,y) = H2(x,y)
from BINOP_1:sch 4();
take
LattStr(# (SubstitutionSet (V,C)),j,m #)
; ( the carrier of LattStr(# (SubstitutionSet (V,C)),j,m #) = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of LattStr(# (SubstitutionSet (V,C)),j,m #) . (A,B) = mi (A \/ B) & the L_meet of LattStr(# (SubstitutionSet (V,C)),j,m #) . (A,B) = mi (A ^ B) ) ) )
thus
( the carrier of LattStr(# (SubstitutionSet (V,C)),j,m #) = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of LattStr(# (SubstitutionSet (V,C)),j,m #) . (A,B) = mi (A \/ B) & the L_meet of LattStr(# (SubstitutionSet (V,C)),j,m #) . (A,B) = mi (A ^ B) ) ) )
by A1, A2; verum