let x, y, c be non pair object ; :: 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) . [<*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) . [<*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) . [<*x,y*>,'&'] = a1 '&' a2 by Lm2; :: thesis: verum

for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds

(Following s) . [<*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) . [<*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) . [<*x,y*>,'&'] = a1 '&' a2 by Lm2; :: thesis: verum