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

proof

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

end;

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