let y, z be Element of L; :: according to WAYBEL_0:def 20 :: thesis: ( not y in R -above x or not y <= z or z in R -above x )
assume A1: ( y in R -above x & y <= z ) ; :: thesis: z in R -above x
then ( R is auxiliary(ii) & x <= x & [x,y] in R ) by WAYBEL_4:14;
then [x,z] in R by A1, WAYBEL_4:def 5;
hence z in R -above x by WAYBEL_4:14; :: thesis: verum