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