let qa, qb be State of (the_reduction_of tfsm); :: according to FSM_1:def 20 :: thesis: ( qa <> qb implies not qa,qb -are_equivalent )
thus ( qa <> qb implies not qa,qb -are_equivalent ) by Th62; :: thesis: verum