for L1, L2 being Lattice
for f being Function of L1,L2 st f is onto holds
for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1