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