let a be Element of L; :: according to WAYBEL_6:def 1 :: thesis: ( not a in (downarrow x) ` or ex b<sub>1</sub> being Element of the carrier of L st
( b<sub>1</sub> in (downarrow x) ` & b₁ is_way_below a ) )
set A = (downarrow x) ` ;
assume a in (downarrow x) ` ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in (downarrow x) ` & b<sub>1</sub> 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