let m be Nat; :: thesis: for S being Language
for phi being wff string of S st phi in (S -formulasOfMaxDepth m) \ (S -formulasOfMaxDepth 0) 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 (S -formulasOfMaxDepth m) \ (S -formulasOfMaxDepth 0) 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 (S -formulasOfMaxDepth m) \ (S -formulasOfMaxDepth 0) 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 (S -formulasOfMaxDepth m) \ (S -formulasOfMaxDepth 0) ; :: 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 Def30, A1; :: thesis: n + 1 <= m
phi is m -wff by B1;
hence n + 1 <= m by A1, Def30; :: thesis: verum