for L1, L2 being C_Lattice st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds
for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 & a1 is_a_complement_of b1 holds
a2 is_a_complement_of b2 by Th9, Th10;