theorem Th9: :: FILTER_2:9

for L1, L2 being 0_Lattice st 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 #) holds
Bottom L1 = Bottom L2