let L1, L2 be 0_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 Bottom L1 = Bottom L2 )
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: Bottom L1 = Bottom L2
then reconsider c = Bottom L1 as Element of L2 ;

now :: thesis: for a being Element of L2 holds
( c "/\" a = c & a "/\" c = c )

let a be Element of L2; :: thesis: ( c "/\" a = c & a "/\" c = c )
reconsider b = a as Element of L1 by A1;
(Bottom L1) "/\" b = Bottom L1 ;
hence c "/\" a = c by A1; :: thesis: a "/\" c = c
hence a "/\" c = c ; :: thesis: verum

end;

hence Bottom L1 = Bottom L2 by LATTICES:def 16; :: thesis: verum