let L be non empty complete Poset; :: thesis: id L is CLHomomorphism of L,L
( id L is directed-sups-preserving & id L is infs-preserving ) by Th3, Th4;
hence id L is CLHomomorphism of L,L by WAYBEL16:def 1; :: thesis: verum