let R be non empty reflexive transitive antisymmetric up-complete TopRelStr ; :: thesis: for S being non empty directed Subset of
for a being Element of st a in S holds
a <= "\/" S,R
let S be non empty directed Subset of ; :: thesis: for a being Element of st a in S holds
a <= "\/" S,R
let a be Element of ; :: 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, LATTICE3:def 9; :: thesis: verum