:: deftheorem defines stable CIRCUIT2:def 6 :
for IIG being non empty non void Circuit-like ManySortedSign
for SCS being non-empty Circuit of IIG
for IT being State of SCS holds
( IT is stable iff IT = Following IT );