let a be Element of L; :: according to WAYBEL_6:def 1 :: thesis: ( not a in (downarrow x) ` or ex b_{1} being Element of the carrier of L st

( b_{1} in (downarrow x) ` & b_{1} is_way_below a ) )

set A = (downarrow x) ` ;

assume a in (downarrow x) ` ; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} in (downarrow x) ` & b_{1} is_way_below a )

then not a in downarrow x by XBOOLE_0:def 5;

then A1: not a <= x by WAYBEL_0:17;

for x being Element of L holds

( not waybelow x is empty & waybelow x is directed ) ;

then consider y being Element of L such that

A2: y << a and

A3: not y <= x by A1, WAYBEL_3:24;

take y ; :: thesis: ( y in (downarrow x) ` & y is_way_below a )

not y in downarrow x by A3, WAYBEL_0:17;

hence y in (downarrow x) ` by XBOOLE_0:def 5; :: thesis: y is_way_below a

thus y is_way_below a by A2; :: thesis: verum

( b

set A = (downarrow x) ` ;

assume a in (downarrow x) ` ; :: thesis: ex b

( b

then not a in downarrow x by XBOOLE_0:def 5;

then A1: not a <= x by WAYBEL_0:17;

for x being Element of L holds

( not waybelow x is empty & waybelow x is directed ) ;

then consider y being Element of L such that

A2: y << a and

A3: not y <= x by A1, WAYBEL_3:24;

take y ; :: thesis: ( y in (downarrow x) ` & y is_way_below a )

not y in downarrow x by A3, WAYBEL_0:17;

hence y in (downarrow x) ` by XBOOLE_0:def 5; :: thesis: y is_way_below a

thus y is_way_below a by A2; :: thesis: verum