let x, y, c be object ; ( x in the carrier of (MajorityStr (x,y,c)) & y in the carrier of (MajorityStr (x,y,c)) & c in the carrier of (MajorityStr (x,y,c)) )
c in the carrier of (1GateCircStr (<*c,x*>,'&'))
by Th43;
then A1:
c in the carrier of (MajorityIStr (x,y,c))
by Th20;
y in the carrier of (1GateCircStr (<*x,y*>,'&'))
by Th43;
then
y in the carrier of ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&')))
by Th20;
then A2:
y in the carrier of (MajorityIStr (x,y,c))
by Th20;
x in the carrier of (1GateCircStr (<*c,x*>,'&'))
by Th43;
then
x in the carrier of (MajorityIStr (x,y,c))
by Th20;
hence
( x in the carrier of (MajorityStr (x,y,c)) & y in the carrier of (MajorityStr (x,y,c)) & c in the carrier of (MajorityStr (x,y,c)) )
by A2, A1, Th20; verum