let z, y be Element of L; :: according to WAYBEL_0:def 19 :: thesis: ( not z in waybelow x or not y <= z or y in waybelow x )
assume z in waybelow x ; :: thesis: ( not y <= z or y in waybelow x )
then z << x by Th7;
then ( y <= z implies y << x ) by Th2;
hence ( y <= z implies y in waybelow x ) ; :: thesis: verum