let B be CLbasis of L; :: thesis: not B is empty
assume A1: B is empty ; :: thesis: contradiction
Top L = "\/" (((waybelow (Top L)) /\ B),L) by Def7
.= Bottom L by A1 ;
hence contradiction by WAYBEL_7:3; :: thesis: verum