let L be non empty reflexive transitive RelStr ; for u, x, y, z being Element of L st u <= x & x << y & y <= z holds
u << z
let u, x, y, z be Element of L; ( u <= x & x << y & y <= z implies u << z )
assume that
A1:
u <= x
and
A2:
for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x <= d )
and
A3:
y <= z
; WAYBEL_3:def 1 u << z
let D be non empty directed Subset of L; WAYBEL_3:def 1 ( z <= sup D implies ex d being Element of L st
( d in D & u <= d ) )
assume
z <= sup D
; ex d being Element of L st
( d in D & u <= d )
then
y <= sup D
by A3, ORDERS_2:3;
then consider d being Element of L such that
A4:
d in D
and
A5:
x <= d
by A2;
take
d
; ( d in D & u <= d )
thus
( d in D & u <= d )
by A1, A4, A5, ORDERS_2:3; verum