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