( x >= Bottom L & Bottom L is compact ) by WAYBEL_3:15, YELLOW_0:44;
then Bottom L in { y where y is Element of L : ( x >= y & y is compact ) } ;
hence not compactbelow x is empty ; :: thesis: verum