let L be non empty reflexive transitive RelStr ; :: thesis: 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; :: thesis: ( 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 ; :: according to WAYBEL_3:def 1 :: thesis: u << z
let D be non empty directed Subset of L; :: according to WAYBEL_3:def 1 :: thesis: ( z <= sup D implies ex d being Element of L st
( d in D & u <= d ) )
assume z <= sup D ; :: thesis: 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 ; :: thesis: ( d in D & u <= d )
thus ( d in D & u <= d ) by A1, A4, A5, ORDERS_2:3; :: thesis: verum