let L be non empty reflexive transitive RelStr ; :: thesis: for X being Subset of L holds

( X is directed iff downarrow X is directed )

let X be Subset of L; :: thesis: ( X is directed iff downarrow X is directed )

thus ( X is directed implies downarrow X is directed ) :: thesis: ( downarrow X is directed implies X is directed )

assume A11: for x, y being Element of L st x in downarrow X & y in downarrow X holds

ex z being Element of L st

( z in downarrow X & x <= z & y <= z ) ; :: according to WAYBEL_0:def 1 :: thesis: X is directed

let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( x in X & y in X implies ex z being Element of L st

( z in X & x <= z & y <= z ) )

assume that

A12: x in X and

A13: y in X ; :: thesis: ex z being Element of L st

( z in X & x <= z & y <= z )

A14: x <= x ;

A15: y <= y ;

A16: x in downarrow X by A12, A14, Def15;

y in downarrow X by A13, A15, Def15;

then consider z being Element of L such that

A17: z in downarrow X and

A18: x <= z and

A19: y <= z by A11, A16;

consider z9 being Element of L such that

A20: z <= z9 and

A21: z9 in X by A17, Def15;

take z9 ; :: thesis: ( z9 in X & x <= z9 & y <= z9 )

thus z9 in X by A21; :: thesis: ( x <= z9 & y <= z9 )

thus ( x <= z9 & y <= z9 ) by A18, A19, A20, ORDERS_2:3; :: thesis: verum

( X is directed iff downarrow X is directed )

let X be Subset of L; :: thesis: ( X is directed iff downarrow X is directed )

thus ( X is directed implies downarrow X is directed ) :: thesis: ( downarrow X is directed implies X is directed )

proof

set Y = downarrow X;
assume A1:
for x, y being Element of L st x in X & y in X holds

ex z being Element of L st

( z in X & x <= z & y <= z ) ; :: according to WAYBEL_0:def 1 :: thesis: downarrow X is directed

let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( x in downarrow X & y in downarrow X implies ex z being Element of L st

( z in downarrow X & x <= z & y <= z ) )

assume that

A2: x in downarrow X and

A3: y in downarrow X ; :: thesis: ex z being Element of L st

( z in downarrow X & x <= z & y <= z )

consider x9 being Element of L such that

A4: x <= x9 and

A5: x9 in X by A2, Def15;

consider y9 being Element of L such that

A6: y <= y9 and

A7: y9 in X by A3, Def15;

consider z being Element of L such that

A8: z in X and

A9: x9 <= z and

A10: y9 <= z by A1, A5, A7;

take z ; :: thesis: ( z in downarrow X & x <= z & y <= z )

z <= z ;

hence z in downarrow X by A8, Def15; :: thesis: ( x <= z & y <= z )

thus ( x <= z & y <= z ) by A4, A6, A9, A10, ORDERS_2:3; :: thesis: verum

end;ex z being Element of L st

( z in X & x <= z & y <= z ) ; :: according to WAYBEL_0:def 1 :: thesis: downarrow X is directed

let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( x in downarrow X & y in downarrow X implies ex z being Element of L st

( z in downarrow X & x <= z & y <= z ) )

assume that

A2: x in downarrow X and

A3: y in downarrow X ; :: thesis: ex z being Element of L st

( z in downarrow X & x <= z & y <= z )

consider x9 being Element of L such that

A4: x <= x9 and

A5: x9 in X by A2, Def15;

consider y9 being Element of L such that

A6: y <= y9 and

A7: y9 in X by A3, Def15;

consider z being Element of L such that

A8: z in X and

A9: x9 <= z and

A10: y9 <= z by A1, A5, A7;

take z ; :: thesis: ( z in downarrow X & x <= z & y <= z )

z <= z ;

hence z in downarrow X by A8, Def15; :: thesis: ( x <= z & y <= z )

thus ( x <= z & y <= z ) by A4, A6, A9, A10, ORDERS_2:3; :: thesis: verum

assume A11: for x, y being Element of L st x in downarrow X & y in downarrow X holds

ex z being Element of L st

( z in downarrow X & x <= z & y <= z ) ; :: according to WAYBEL_0:def 1 :: thesis: X is directed

let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( x in X & y in X implies ex z being Element of L st

( z in X & x <= z & y <= z ) )

assume that

A12: x in X and

A13: y in X ; :: thesis: ex z being Element of L st

( z in X & x <= z & y <= z )

A14: x <= x ;

A15: y <= y ;

A16: x in downarrow X by A12, A14, Def15;

y in downarrow X by A13, A15, Def15;

then consider z being Element of L such that

A17: z in downarrow X and

A18: x <= z and

A19: y <= z by A11, A16;

consider z9 being Element of L such that

A20: z <= z9 and

A21: z9 in X by A17, Def15;

take z9 ; :: thesis: ( z9 in X & x <= z9 & y <= z9 )

thus z9 in X by A21; :: thesis: ( x <= z9 & y <= z9 )

thus ( x <= z9 & y <= z9 ) by A18, A19, A20, ORDERS_2:3; :: thesis: verum