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
A2: s1 is stable and
A3: ex n being Element of NAT st s1 = Following (s,n) and
A4: s2 is stable and
A5: ex n being Element of NAT st s2 = Following (s,n) ; :: thesis: s1 = s2
consider n1 being Element of NAT such that
A6: s1 = Following (s,n1) by A3;
consider n2 being Element of NAT such that
A7: s2 = Following (s,n2) by A5;
per cases ( n1 <= n2 or n2 <= n1 ) ;
suppose n1 <= n2 ; :: thesis: s1 = s2
hence s1 = s2 by A2, A6, A7, CIRCCMB2:4; :: thesis: verum
end;
suppose n2 <= n1 ; :: thesis: s1 = s2
hence s1 = s2 by A4, A6, A7, CIRCCMB2:4; :: thesis: verum
end;
end;