set L = Normal_forms_on A;
deffunc H1( Element of Normal_forms_on A, Element of Normal_forms_on A) -> Element of Normal_forms_on A = mi (\$1 \/ \$2);
consider j being BinOp of () such that
A1: for x, y being Element of Normal_forms_on A holds j . (x,y) = H1(x,y) from deffunc H2( Element of Normal_forms_on A, Element of Normal_forms_on A) -> Element of Normal_forms_on A = mi (\$1 ^ \$2);
consider m being BinOp of () such that
A2: for x, y being Element of Normal_forms_on A holds m . (x,y) = H2(x,y) from take LattStr(# (),j,m #) ; :: thesis: ( the carrier of LattStr(# (),j,m #) = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of LattStr(# (),j,m #) . (B,C) = mi (B \/ C) & the L_meet of LattStr(# (),j,m #) . (B,C) = mi (B ^ C) ) ) )

thus ( the carrier of LattStr(# (),j,m #) = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of LattStr(# (),j,m #) . (B,C) = mi (B \/ C) & the L_meet of LattStr(# (),j,m #) . (B,C) = mi (B ^ C) ) ) ) by A1, A2; :: thesis: verum