set I = AR -below x;
[(Bottom L),x] in AR by Def7;
then Bottom L in AR -below x ;
hence not AR -below x is empty ; :: thesis: verum