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