let IT1, IT2 be Nat; ( phi is IT1 -wff & ( for n being Nat st phi is n -wff holds
IT1 <= n ) & phi is IT2 -wff & ( for n being Nat st phi is n -wff holds
IT2 <= n ) implies IT1 = IT2 )
assume A4:
( phi is IT1 -wff & ( for n being Nat st phi is n -wff holds
IT1 <= n ) )
; ( not phi is IT2 -wff or ex n being Nat st
( phi is n -wff & not IT2 <= n ) or IT1 = IT2 )
assume A5:
( phi is IT2 -wff & ( for n being Nat st phi is n -wff holds
IT2 <= n ) )
; IT1 = IT2
A6:
IT2 <= IT1
by A5, A4;
IT1 <= IT2
by A4, A5;
hence
IT1 = IT2
by A6, XXREAL_0:1; verum