let v be Element of L; :: according to WAYBEL12:def 4 :: thesis: ( v <> Bottom L implies (Top L) "/\" v <> Bottom L )
assume v <> Bottom L ; :: thesis: (Top L) "/\" v <> Bottom L
hence (Top L) "/\" v <> Bottom L by WAYBEL_1:5; :: thesis: verum