let L, S, T be non empty complete Poset; :: thesis: 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; :: thesis: for g being CLHomomorphism of S,T holds g * f is CLHomomorphism of L,T
let g be CLHomomorphism of S,T; :: thesis: 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; :: thesis: verum