let L be non empty reflexive transitive RelStr ; for X being Subset of L holds
( X is directed iff downarrow X is directed )
let X be Subset of L; ( X is directed iff downarrow X is directed )
thus
( X is directed implies downarrow X is directed )
( downarrow X is directed implies X is directed )proof
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 )
;
WAYBEL_0:def 1 downarrow X is directed
let x,
y be
Element of
L;
WAYBEL_0:def 1 ( 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
;
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
;
( z in downarrow X & x <= z & y <= z )
z <= z
;
hence
z in downarrow X
by A8, Def15;
( x <= z & y <= z )
thus
(
x <= z &
y <= z )
by A4, A6, A9, A10, ORDERS_2:3;
verum
end;
set Y = downarrow X;
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 )
; WAYBEL_0:def 1 X is directed
let x, y be Element of L; WAYBEL_0:def 1 ( 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
; 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
; ( z9 in X & x <= z9 & y <= z9 )
thus
z9 in X
by A21; ( x <= z9 & y <= z9 )
thus
( x <= z9 & y <= z9 )
by A18, A19, A20, ORDERS_2:3; verum