let L be non empty reflexive transitive RelStr ; for X being Subset of holds
( X is directed iff downarrow X is directed )
let X be Subset of ; ( 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 st
x in X &
y in X holds
ex
z being
Element of st
(
z in X &
x <= z &
y <= z )
;
WAYBEL_0:def 1 downarrow X is directed
let x,
y be
Element of ;
WAYBEL_0:def 1 ( x in downarrow X & y in downarrow X implies ex z being Element of 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 st
( z in downarrow X & x <= z & y <= z )
consider x' being
Element of
such that A4:
x <= x'
and A5:
x' in X
by A2, Def15;
consider y' being
Element of
such that A6:
y <= y'
and A7:
y' in X
by A3, Def15;
consider z being
Element of
such that A8:
z in X
and A9:
x' <= z
and A10:
y' <= 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:26;
verum
end;
set Y = downarrow X;
assume A11:
for x, y being Element of st x in downarrow X & y in downarrow X holds
ex z being Element of st
( z in downarrow X & x <= z & y <= z )
; WAYBEL_0:def 1 X is directed
let x, y be Element of ; WAYBEL_0:def 1 ( x in X & y in X implies ex z being Element of st
( z in X & x <= z & y <= z ) )
assume that
A12:
x in X
and
A13:
y in X
; ex z being Element of 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 such that
A17:
z in downarrow X
and
A18:
x <= z
and
A19:
y <= z
by A11, A16;
consider z' being Element of such that
A20:
z <= z'
and
A21:
z' in X
by A17, Def15;
take
z'
; ( z' in X & x <= z' & y <= z' )
thus
z' in X
by A21; ( x <= z' & y <= z' )
thus
( x <= z' & y <= z' )
by A18, A19, A20, ORDERS_2:26; verum