let L be Lattice; :: thesis: ( 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 #) )
consider o1, o2 being BinOp of (.L.> such that
A1: ( o1 = the L_join of L || (.L.> & o2 = the L_meet of L || (.L.> & latt L,(.L.> = LattStr(# (.L.>,o1,o2 #) ) by Def16;
A2: ( dom H₂(L) = [:H₁(L),H₁(L):] & dom H₃(L) = [:H₁(L),H₁(L):] ) by FUNCT_2:def 1;
( H₂(L) | (dom H₂(L)) = H₂(L) & H₃(L) | (dom H₃(L)) = H₃(L) ) by RELAT_1:97;
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, A2; :: thesis: verum