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