let L1, L2, L3 be Lattice; :: thesis: ( L1,L2 are_isomorphic & L2,L3 are_isomorphic implies L1,L3 are_isomorphic )
assume ( LattRel L1, LattRel L2 are_isomorphic & LattRel L2, LattRel L3 are_isomorphic ) ; :: according to FILTER_1:def 9 :: thesis: L1,L3 are_isomorphic
hence LattRel L1, LattRel L3 are_isomorphic by WELLORD1:52; :: according to FILTER_1:def 9 :: thesis: verum