let x, y, c be object ; :: thesis: ( 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; :: thesis: verum

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; :: thesis: verum