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 that
A1: y in R -above x and
A2: y <= z ; :: thesis: z in R -above x
( x <= x & [x,y] in R ) by A1, WAYBEL_4:14;
then [x,z] in R by A2, WAYBEL_4:def 4;
hence z in R -above x by WAYBEL_4:14; :: thesis: verum