set F = S -firstChar ;
let w be string of S; :: thesis: ( w is exal implies not w is 0wff )
assume w is exal ; :: thesis: not w is 0wff
then (S -firstChar) . w is literal by DefExal;
hence not w is 0wff ; :: thesis: verum