let x, y, c be set ; :: 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