let L be complete LATTICE; :: thesis: ( LowerAdj (id L) = id L & UpperAdj (id L) = id L )
[(id L),(id L)] is Galois by Th6;
hence ( LowerAdj (id L) = id L & UpperAdj (id L) = id L ) by Def1, Def2; :: thesis: verum