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 A1: ( X c= Y & ex_inf_of X,L & 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 x in X ; :: thesis: "/\" Y,L <= x
then ( x in Y & "/\" Y,L is_<=_than Y ) by A1, Def10;
hence "/\" Y,L <= x by LATTICE3:def 8; :: thesis: verum

end;

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