let L be Lattice; ( latt (L,(.L.>) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & latt (L,<.L.)) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) )
A1:
( dom H3(L) = [:H1(L),H1(L):] & H2(L) | (dom H2(L)) = H2(L) )
by FUNCT_2:def 1, RELAT_1:68;
( ex o1, o2 being BinOp of (.L.> st
( o1 = the L_join of L || (.L.> & o2 = the L_meet of L || (.L.> & latt (L,(.L.>) = LattStr(# (.L.>,o1,o2 #) ) & dom H2(L) = [:H1(L),H1(L):] )
by Def14, FUNCT_2:def 1;
hence
( latt (L,(.L.>) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & latt (L,<.L.)) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) )
by A1, RELAT_1:68; verum