let IT1, IT2 be Nat; :: thesis: ( 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 ) ) ; :: thesis: ( 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 ) ) ; :: thesis: IT1 = IT2

A6: IT2 <= IT1 by A5, A4;

IT1 <= IT2 by A4, A5;

hence IT1 = IT2 by A6, XXREAL_0:1; :: thesis: verum

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 ) ) ; :: thesis: ( 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 ) ) ; :: thesis: IT1 = IT2

A6: IT2 <= IT1 by A5, A4;

IT1 <= IT2 by A4, A5;

hence IT1 = IT2 by A6, XXREAL_0:1; :: thesis: verum