theorem :: FILTER_1:49
for L1, L2 being Lattice holds [:L1,L2:],[:L2,L1:] are_isomorphic