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

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