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 A1: ( x1 in AR -below x & y1 <= x1 ) ; :: thesis: y1 in AR -below x
then consider v1 being Element of L such that
A2: ( v1 = x1 & [v1,x] in AR ) ;
x <= x ;
then [y1,x] in AR by A1, A2, Def5;
hence y1 in AR -below x ; :: thesis: verum