theorem :: FSCIRC_1:14

for x, y, c being non pair set
for s being State of (BorrowCirc (x,y,c))
for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds
(Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2