let S be Language; :: thesis: for phi being wff string of S st not phi is 0wff holds
Depth phi <> 0
let phi be wff string of S; :: thesis: ( not phi is 0wff implies Depth phi <> 0 )
assume not phi is 0wff ; :: thesis: Depth phi <> 0
then not phi is 0 -wff ;
hence Depth phi <> 0 by Def30; :: thesis: verum