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

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