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 )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 )
;
:: 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 x' being
Element of
L such that A4:
x <= x'
and A5:
x' in X
by A2, Def15;
consider y' being
Element of
L such that A6:
y <= y'
and A7:
y' in X
by A3, Def15;
consider z being
Element of
L such that A8:
z in X
and A9:
x' <= z
and A10:
y' <= 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:26;
:: thesis: 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 )
; :: 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 z' being Element of L such that
A20:
z <= z'
and
A21:
z' in X
by A17, Def15;
take
z'
; :: thesis: ( z' in X & x <= z' & y <= z' )
thus
z' in X
by A21; :: thesis: ( x <= z' & y <= z' )
thus
( x <= z' & y <= z' )
by A18, A19, A20, ORDERS_2:26; :: thesis: verum