let L, S, T be non empty complete Poset; for f being CLHomomorphism of L,S
for g being CLHomomorphism of S,T holds g * f is CLHomomorphism of L,T
let f be CLHomomorphism of L,S; for g being CLHomomorphism of S,T holds g * f is CLHomomorphism of L,T
let g be CLHomomorphism of S,T; g * f is CLHomomorphism of L,T
( f is directed-sups-preserving & g is directed-sups-preserving )
by WAYBEL16:def 1;
then A1:
g * f is directed-sups-preserving
by WAYBEL20:28;
( f is infs-preserving & g is infs-preserving )
by WAYBEL16:def 1;
then
g * f is infs-preserving
by WAYBEL20:25;
hence
g * f is CLHomomorphism of L,T
by A1, WAYBEL16:def 1; verum