for C being complete Lattice
for a, b being Element of C st C is I_Lattice holds
a => b = "\/" ( { c where c is Element of C : a "/\" c [= b } ,C)