let s1, s2 be State of A; :: thesis: ( s1 is stable & ex n being Element of NAT st s1 = Following s,n & s2 is stable & ex n being Element of NAT st s2 = Following s,n implies s1 = s2 )
assume that
A3: ( s1 is stable & ex n being Element of NAT st s1 = Following s,n ) and
A4: ( s2 is stable & ex n being Element of NAT st s2 = Following s,n ) ; :: thesis: s1 = s2
consider n1 being Element of NAT such that
A5: s1 = Following s,n1 by A3;
consider n2 being Element of NAT such that
A6: s2 = Following s,n2 by A4;

per cases ( n1 <= n2 or n2 <= n1 ) ;

suppose n1 <= n2 ; :: thesis: s1 = s2

hence s1 = s2 by A3, A5, A6, CIRCCMB2:4; :: thesis: verum

end;

suppose n2 <= n1 ; :: thesis: s1 = s2

hence s1 = s2 by A4, A5, A6, CIRCCMB2:4; :: thesis: verum

end;

end;