for L1, L2 being complete LATTICE
for T1 being Scott TopAugmentation of L1
for T2 being Scott TopAugmentation of L2 st L1,L2 are_isomorphic & T1 is injective holds
T2 is injective by Th5, Th6;