let IT1, IT2 be Nat; :: thesis: ( t is IT1 -termal & ( for n being Nat st t is n -termal holds
IT1 <= n ) & t is IT2 -termal & ( for n being Nat st t is n -termal holds
IT2 <= n ) implies IT1 = IT2 )
set phi = t;
assume A4: ( t is IT1 -termal & ( for n being Nat st t is n -termal holds
IT1 <= n ) ) ; :: thesis: ( not t is IT2 -termal or ex n being Nat st
( t is n -termal & not IT2 <= n ) or IT1 = IT2 )
assume A5: ( t is IT2 -termal & ( for n being Nat st t is n -termal 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