let m be Nat; :: thesis: for S being Language
for phi being wff string of S st phi in () \ () holds
ex n being Nat st
( phi is n + 1 -wff & not phi is n -wff & n + 1 <= m )

let S be Language; :: thesis: for phi being wff string of S st phi in () \ () holds
ex n being Nat st
( phi is n + 1 -wff & not phi is n -wff & n + 1 <= m )

let phi be wff string of S; :: thesis: ( phi in () \ () implies ex n being Nat st
( phi is n + 1 -wff & not phi is n -wff & n + 1 <= m ) )

set Phim = S -formulasOfMaxDepth m;
set Phi0 = S -formulasOfMaxDepth 0;
assume B1: phi in () \ () ; :: thesis: ex n being Nat st
( phi is n + 1 -wff & not phi is n -wff & n + 1 <= m )

then not phi in S -formulasOfMaxDepth 0 by XBOOLE_0:def 5;
then not phi is 0 -wff ;
then Depth phi <> 0 by Def30;
then consider n being Nat such that
A1: Depth phi = n + 1 by NAT_1:6;
take n ; :: thesis: ( phi is n + 1 -wff & not phi is n -wff & n + 1 <= m )
not n + 1 <= n + 0 by XREAL_1:8;
hence ( phi is n + 1 -wff & not phi is n -wff ) by ; :: thesis: n + 1 <= m
phi is m -wff by B1;
hence n + 1 <= m by ; :: thesis: verum