theorem :: FSCIRC_1:15

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