let it1, it2 be a_partition of the carrier of tfsm; ( it1 is final & it2 is final implies it1 = it2 )
assume that
A2:
it1 is final
and
A3:
it2 is final
; it1 = it2
now not it1 <> it2assume
it1 <> it2
;
contradictionthen
not for
X being
object 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 )
;
contradictionend; suppose A21:
( not
X in it1 &
X in it2 )
;
contradictionend; end; end;
hence
it1 = it2
; verum