let x, y, c be non pair object ; for s being State of (MajorityCirc (x,y,c))
for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds
(Following (s,2)) . [<*c,x*>,'&'] = a3 '&' a1
reconsider a = y as Vertex of (MajorityStr (x,y,c)) by Th72;
let s be State of (MajorityCirc (x,y,c)); for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds
(Following (s,2)) . [<*c,x*>,'&'] = a3 '&' a1
s . a is Element of BOOLEAN
;
hence
for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds
(Following (s,2)) . [<*c,x*>,'&'] = a3 '&' a1
by Lm3; verum