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;
"/\" (X,L) <= x by A2, YELLOW_2:22;
hence "/\" (X,L) <= y by A3, YELLOW_0:def 2; :: thesis: verum

end;

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