let L1, L2 be non empty LattStr ; :: 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 holds
( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) )
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 holds
( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) )
let a1, b1 be Element of L1; :: thesis: for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds
( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) )
let a2, b2 be Element of L2; :: thesis: ( a1 = a2 & b1 = b2 implies ( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) )
assume A2: ( a1 = a2 & b1 = b2 ) ; :: thesis: ( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) )
thus a1 "\/" b1 = a2 "\/" b2 by A1, A2; :: thesis: ( a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) )
thus a1 "/\" b1 = a2 "/\" b2 by A1, A2; :: thesis: ( ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) )
( ( a1 [= b1 implies a1 "\/" b1 = b1 ) & ( a1 "\/" b1 = b1 implies a1 [= b1 ) & ( a2 "\/" b2 = b2 implies a2 [= b2 ) & ( a2 [= b2 implies a2 "\/" b2 = b2 ) ) by LATTICES:def 3;
hence ( a1 [= b1 iff a2 [= b2 ) by A1, A2; :: thesis: verum