theorem Th13: :: FSCIRC_1:13

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