let L be complete LATTICE; :: thesis: for X, Y being Subset of L st Y is_coarser_than X holds
"/\" X,L <= "/\" Y,L
let X, Y be Subset of L; :: thesis: ( Y is_coarser_than X implies "/\" X,L <= "/\" Y,L )
assume A1: Y is_coarser_than X ; :: thesis: "/\" X,L <= "/\" Y,L
"/\" X,L is_<=_than Y

proof

let y be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not y in Y or "/\" X,L <= y )
assume y in Y ; :: thesis: "/\" X,L <= y
then consider x being Element of L such that
A2: x in X and
A3: x <= y by A1, YELLOW_4:def 2;
"/\" X,L <= x by A2, YELLOW_2:24;
hence "/\" X,L <= y by A3, YELLOW_0:def 2; :: thesis: verum

end;

hence "/\" X,L <= "/\" Y,L by YELLOW_0:33; :: thesis: verum