deffunc H₁( Element of L, Element of L) -> Element of L = $1 *' $2;
consider K being BinOp of the carrier of L such that
A1: for a, b being Element of L holds K . (a,b) = H₁(a,b) from BINOP_1:sch 4();
take OrthoLattStr(# the carrier of L, the L_join of L,K, the Compl of L #) ; :: thesis: ( the carrier of OrthoLattStr(# the carrier of L, the L_join of L,K, the Compl of L #) = the carrier of L & the L_join of OrthoLattStr(# the carrier of L, the L_join of L,K, the Compl of L #) = the L_join of L & the Compl of OrthoLattStr(# the carrier of L, the L_join of L,K, the Compl of L #) = the Compl of L & ( for a, b being Element of L holds the L_meet of OrthoLattStr(# the carrier of L, the L_join of L,K, the Compl of L #) . (a,b) = a *' b ) )
thus ( the carrier of OrthoLattStr(# the carrier of L, the L_join of L,K, the Compl of L #) = the carrier of L & the L_join of OrthoLattStr(# the carrier of L, the L_join of L,K, the Compl of L #) = the L_join of L & the Compl of OrthoLattStr(# the carrier of L, the L_join of L,K, the Compl of L #) = the Compl of L & ( for a, b being Element of L holds the L_meet of OrthoLattStr(# the carrier of L, the L_join of L,K, the Compl of L #) . (a,b) = a *' b ) ) by A1; :: thesis: verum