let x be Element of L; :: according to WAYBEL_4:def 6 :: thesis: [(Bottom L),x] in L -waybelow
Bottom L << x by WAYBEL_3:4;
hence [(Bottom L),x] in L -waybelow by Def1; :: thesis: verum