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