let it1, it2 be a_partition of the carrier of tfsm; :: thesis: ( it1 is final & it2 is final implies it1 = it2 )
assume A3: ( it1 is final & it2 is final ) ; :: thesis: it1 = it2

now

assume it1 <> it2 ; :: thesis: contradiction
then not for X being set holds
( X in it1 iff X in it2 ) by TARSKI:2;
then consider X being set such that
A4: ( ( X in it1 & not X in it2 ) or ( not X in it1 & X in it2 ) ) ;

per cases ( ( X in it1 & not X in it2 ) or ( not X in it1 & X in it2 ) ) by A4;

suppose A5: ( X in it1 & not X in it2 ) ; :: thesis: contradiction

then reconsider X = X as Subset of tfsm ;
consider qx being Element of tfsm such that
A6: qx in X by A5, Th11;
union it2 = the carrier of tfsm by EQREL_1:def 6;
then consider Z being set such that
A7: ( qx in Z & Z in it2 ) by TARSKI:def 4;
reconsider Z = Z as Subset of tfsm by A7;
set XZ = X \ Z;
set ZX = Z \ X;
set Y' = (X \ Z) \/ (Z \ X);
(X \ Z) \/ (Z \ X) <> {}

proof

assume (X \ Z) \/ (Z \ X) = {} ; :: thesis: contradiction
then ( X \ Z = {} & Z \ X = {} ) ;
then ( X c= Z & Z c= X ) by XBOOLE_1:37;
hence contradiction by A5, A7, XBOOLE_0:def 10; :: thesis: verum

end;

then consider qy being Element of tfsm such that
A8: qy in (X \ Z) \/ (Z \ X) by SUBSET_1:10;
reconsider X = X as Element of it1 by A5;

A9: now

assume A10: qy in X \ Z ; :: thesis: contradiction
then A11: ( qy in X & not qy in Z ) by XBOOLE_0:def 5;
not qx,qy -are_equivalent

proof

assume qx,qy -are_equivalent ; :: thesis: contradiction
then consider Z' being Element of it2 such that
A12: ( qx in Z' & qy in Z' ) by A3, Def14;

per cases ( Z = Z' or Z <> Z' ) ;

suppose Z = Z' ; :: thesis: contradiction

hence contradiction by A10, A12, XBOOLE_0:def 5; :: thesis: verum

end;

suppose Z <> Z' ; :: thesis: contradiction

then Z misses Z' by A7, EQREL_1:def 6;
then Z /\ Z' = {} by XBOOLE_0:def 7;
hence contradiction by A7, A12, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence contradiction by A3, A6, A11, Def14; :: thesis: verum

end;

now

assume A13: qy in Z \ X ; :: thesis: contradiction
then A14: ( qy in Z & not qy in X ) by XBOOLE_0:def 5;
not qx,qy -are_equivalent

proof

assume qx,qy -are_equivalent ; :: thesis: contradiction
then consider Z' being Element of it1 such that
A15: ( qx in Z' & qy in Z' ) by A3, Def14;

per cases ( X = Z' or X <> Z' ) ;

suppose X = Z' ; :: thesis: contradiction

hence contradiction by A13, A15, XBOOLE_0:def 5; :: thesis: verum

end;

suppose X <> Z' ; :: thesis: contradiction

then X misses Z' by EQREL_1:def 6;
then X /\ Z' = {} by XBOOLE_0:def 7;
hence contradiction by A6, A15, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence contradiction by A3, A7, A14, Def14; :: thesis: verum

end;

hence contradiction by A8, A9, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A16: ( not X in it1 & X in it2 ) ; :: thesis: contradiction

then reconsider X = X as Subset of tfsm ;
consider qx being Element of tfsm such that
A17: qx in X by A16, Th11;
union it1 = the carrier of tfsm by EQREL_1:def 6;
then consider Z being set such that
A18: ( qx in Z & Z in it1 ) by TARSKI:def 4;
reconsider Z = Z as Subset of tfsm by A18;
set XZ = X \ Z;
set ZX = Z \ X;
set Y' = (X \ Z) \/ (Z \ X);
(X \ Z) \/ (Z \ X) <> {}

proof

assume (X \ Z) \/ (Z \ X) = {} ; :: thesis: contradiction
then ( X \ Z = {} & Z \ X = {} ) ;
then ( X c= Z & Z c= X ) by XBOOLE_1:37;
hence contradiction by A16, A18, XBOOLE_0:def 10; :: thesis: verum

end;

then consider qy being Element of tfsm such that
A19: qy in (X \ Z) \/ (Z \ X) by SUBSET_1:10;
reconsider X = X as Element of it2 by A16;

A20: now

assume A21: qy in X \ Z ; :: thesis: contradiction
then A22: ( qy in X & not qy in Z ) by XBOOLE_0:def 5;
not qx,qy -are_equivalent

proof

assume qx,qy -are_equivalent ; :: thesis: contradiction
then consider Z' being Element of it1 such that
A23: ( qx in Z' & qy in Z' ) by A3, Def14;

per cases ( Z = Z' or Z <> Z' ) ;

suppose Z = Z' ; :: thesis: contradiction

hence contradiction by A21, A23, XBOOLE_0:def 5; :: thesis: verum

end;

suppose Z <> Z' ; :: thesis: contradiction

then Z misses Z' by A18, EQREL_1:def 6;
then Z /\ Z' = {} by XBOOLE_0:def 7;
hence contradiction by A18, A23, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence contradiction by A3, A17, A22, Def14; :: thesis: verum

end;

now

assume A24: qy in Z \ X ; :: thesis: contradiction
then A25: ( qy in Z & not qy in X ) by XBOOLE_0:def 5;
not qx,qy -are_equivalent

proof

assume qx,qy -are_equivalent ; :: thesis: contradiction
then consider Z' being Element of it2 such that
A26: ( qx in Z' & qy in Z' ) by A3, Def14;

per cases ( X = Z' or X <> Z' ) ;

suppose X = Z' ; :: thesis: contradiction

hence contradiction by A24, A26, XBOOLE_0:def 5; :: thesis: verum

end;

suppose X <> Z' ; :: thesis: contradiction

then X misses Z' by EQREL_1:def 6;
then X /\ Z' = {} by XBOOLE_0:def 7;
hence contradiction by A17, A26, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence contradiction by A3, A18, A25, Def14; :: thesis: verum

end;

hence contradiction by A19, A20, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence it1 = it2 ; :: thesis: verum