set I = AR -below x;
let x1, y1 be Element of L; :: according to WAYBEL_0:def 19 :: thesis: ( not x1 in AR -below x or not y1 <= x1 or y1 in AR -below x )
assume that
A1: x1 in AR -below x and
A2: y1 <= x1 ; :: thesis: y1 in AR -below x
A3: ex v1 being Element of L st
( v1 = x1 & [v1,x] in AR ) by A1;
x <= x ;
then [y1,x] in AR by A2, A3, Def4;
hence y1 in AR -below x ; :: thesis: verum