theorem Th65: :: WAYBEL34:65

for S, T being lower-bounded LATTICE
for f being finite-sups-preserving Function of S,T
for S9 being non empty full finite-sups-inheriting SubRelStr of S
for T9 being non empty full finite-sups-inheriting SubRelStr of T
for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is finite-sups-preserving