let R be non empty reflexive transitive antisymmetric with_suprema RelStr ; :: thesis: for D being directed lower Subset of R
for x, y being Element of R st x in D & y in D holds
x "\/" y in D
let D be directed lower Subset of R; :: thesis: for x, y being Element of R st x in D & y in D holds
x "\/" y in D
let x, y be Element of R; :: thesis: ( x in D & y in D implies x "\/" y in D )
assume ( x in D & y in D ) ; :: thesis: x "\/" y in D
then consider z being Element of R such that
A1: ( z in D & x <= z & y <= z ) by WAYBEL_0:def 1;
x "\/" y <= z by A1, YELLOW_0:22;
hence x "\/" y in D by A1, WAYBEL_0:def 19; :: thesis: verum