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

end;

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