:: deftheorem defines are_isomorphic FILTER_1:def 9 :
for L1, L2 being Lattice holds
( L1,L2 are_isomorphic iff LattRel L1, LattRel L2 are_isomorphic );