theorem :: FSCIRC_1:4

for x, y, c being set
for s being State of (BorrowICirc (x,y,c))
for a, b being Element of BOOLEAN st a = s . y & b = s . c holds
(Following s) . [<*y,c*>,and2] = a '&' b