let R be non empty reflexive transitive antisymmetric up-complete TopRelStr ; :: thesis: for S being non empty directed Subset of R
for a being Element of R st a in S holds
a <= "\/" (S,R)
let S be non empty directed Subset of R; :: thesis: for a being Element of R st a in S holds
a <= "\/" (S,R)
let a be Element of R; :: thesis: ( a in S implies a <= "\/" (S,R) )
assume A1: a in S ; :: thesis: a <= "\/" (S,R)
ex_sup_of S,R by WAYBEL_0:75;
then S is_<=_than "\/" (S,R) by YELLOW_0:30;
hence a <= "\/" (S,R) by A1; :: thesis: verum