set S = the carrier of tfsm;
defpred S₁[ object , object ] means ex qa, qb being Element of the carrier of tfsm st
( qa = $1 & qb = $2 & i -equivalent qa,qb );
A1: for x, y being object st S₁[x,y] holds
S₁[y,x] by Th22;
A2: for x, y, z being object st S₁[x,y] & S₁[y,z] holds
S₁[x,z] by Th23;
A3: for x being object st x in the carrier of tfsm holds
S₁[x,x] by Th21;
consider EqR being Equivalence_Relation of the carrier of tfsm such that
A4: for x, y being object holds
( [x,y] in EqR iff ( x in the carrier of tfsm & y in the carrier of tfsm & S₁[x,y] ) ) from EQREL_1:sch 1(A3, A1, A2);
take EqR ; :: thesis: for qa, qb being State of tfsm holds
( [qa,qb] in EqR iff i -equivalent qa,qb )
let qa, qb be Element of the carrier of tfsm; :: thesis: ( [qa,qb] in EqR iff i -equivalent qa,qb )

hereby :: thesis: ( i -equivalent qa,qb implies [qa,qb] in EqR )

assume [qa,qb] in EqR ; :: thesis: i -equivalent qa,qb
then ex qa9, qb9 being Element of the carrier of tfsm st
( qa9 = qa & qb9 = qb & i -equivalent qa9,qb9 ) by A4;
hence i -equivalent qa,qb ; :: thesis: verum

end;

assume i -equivalent qa,qb ; :: thesis: [qa,qb] in EqR
hence [qa,qb] in EqR by A4; :: thesis: verum