let L be RelStr ; :: thesis: for X being set
for a being Element of L st a in X & ex_inf_of X,L holds
"/\" (X,L) <= a
let X be set ; :: thesis: for a being Element of L st a in X & ex_inf_of X,L holds
"/\" (X,L) <= a
let a be Element of L; :: thesis: ( a in X & ex_inf_of X,L implies "/\" (X,L) <= a )
assume that
A1: a in X and
A2: ex_inf_of X,L ; :: thesis: "/\" (X,L) <= a
X is_>=_than "/\" (X,L) by A2, YELLOW_0:def 10;
hence "/\" (X,L) <= a by A1; :: thesis: verum