:: deftheorem defines are_isomorphic LATTICE4:def 3 :
for L1, L2 being Lattice holds
( L1,L2 are_isomorphic iff ex f being Homomorphism of L1,L2 st f is bijective );