deffunc H₁( 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 = H₁(x,y) from BINOP_1:sch 4();
deffunc H₂( 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 = H₂(x,y) from BINOP_1:sch 4();
take LattStr(# (SubstitutionSet V,C),j,m #) ; :: thesis: ( 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; :: thesis: verum