for L being complete continuous LATTICE st ( for l being Element of L ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) ) ) holds
for l being Element of L holds l = "\/" (((waybelow l) /\ (PRIME (L opp))),L)