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; :: thesis: verum