let L1, L2 be C_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 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 )
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 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
let a1, b1 be Element of L1; :: thesis: 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
let a2, b2 be Element of L2; :: thesis: ( a1 = a2 & b1 = b2 & a1 is_a_complement_of b1 implies a2 is_a_complement_of b2 )
assume ( a1 = a2 & b1 = b2 ) ; :: thesis: ( not a1 is_a_complement_of b1 or a2 is_a_complement_of b2 )
then A2: ( a2 "\/" b2 = a1 "\/" b1 & a2 "/\" b2 = a1 "/\" b1 ) by A1;
assume a1 is_a_complement_of b1 ; :: thesis: a2 is_a_complement_of b2
then ( a1 "\/" b1 = Top L1 & a1 "/\" b1 = Bottom L1 ) by LATTICES:def 18;
hence ( a2 "\/" b2 = Top L2 & b2 "\/" a2 = Top L2 & a2 "/\" b2 = Bottom L2 & b2 "/\" a2 = Bottom L2 ) by A1, A2, Th9, Th10; :: according to LATTICES:def 18 :: thesis: verum