theorem :: LATTICE3:44

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