theorem :: FACIRC_1:76
for x, y, c being non pair object
for s being State of (MajorityCirc (x,y,c))
for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds
(Following s) . [<*x,y*>,'&'] = a1 '&' a2