let x, y, c be non pair set ; :: thesis: 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,2) . [<*x,y*>,'&' ] = a1 '&' a2
reconsider a = c as Vertex of (MajorityStr x,y,c) by Th72;
let s be State of (MajorityCirc x,y,c); :: thesis: for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds
(Following s,2) . [<*x,y*>,'&' ] = a1 '&' a2
s . a is Element of BOOLEAN ;
hence for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds
(Following s,2) . [<*x,y*>,'&' ] = a1 '&' a2 by Lm3; :: thesis: verum