let L1, L2 be B_Lattice; :: thesis: ( 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 #) implies for a being Element of L1
for b being Element of L2 st a = b holds
a ` = b ` )
assume A1: 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 #) ; :: thesis: for a being Element of L1
for b being Element of L2 st a = b holds
a ` = b `
let a be Element of L1; :: thesis: for b being Element of L2 st a = b holds
a ` = b `
let b be Element of L2; :: thesis: ( a = b implies a ` = b ` )
assume A2: a = b ; :: thesis: a ` = b `
reconsider b9 = a ` as Element of L2 by A1;
a ` is_a_complement_of a by LATTICES:def 21;
then b9 is_a_complement_of b by A1, A2, Th11;
hence a ` = b ` by LATTICES:def 21; :: thesis: verum