theorem Th6: :: LATTICE4:6
for L1, L2 being Lattice
for f being Function of the carrier of L1, the carrier of L2 st f is onto holds
for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1