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, LATTICE3:def 8; :: thesis: verum