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 and
A2: ( x <= z & y <= z ) by WAYBEL_0:def 1;
x "\/" y <= z by A2, YELLOW_0:22;
hence x "\/" y in D by A1, WAYBEL_0:def 19; :: thesis: verum