let L be RelStr ; :: thesis: for X, Y being set st X c= Y & ex_inf_of X,L & ex_inf_of Y,L holds
"/\" (X,L) >= "/\" (Y,L)
let X, Y be set ; :: thesis: ( X c= Y & ex_inf_of X,L & ex_inf_of Y,L implies "/\" (X,L) >= "/\" (Y,L) )
assume that
A1: X c= Y and
A2: ex_inf_of X,L and
A3: ex_inf_of Y,L ; :: thesis: "/\" (X,L) >= "/\" (Y,L)
"/\" (Y,L) is_<=_than X

proof

let x be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not x in X or "/\" (Y,L) <= x )
assume A4: x in X ; :: thesis: "/\" (Y,L) <= x
"/\" (Y,L) is_<=_than Y by A3, Def10;
hence "/\" (Y,L) <= x by A1, A4; :: thesis: verum

end;

hence "/\" (X,L) >= "/\" (Y,L) by A2, Def10; :: thesis: verum