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) )
y in the carrier of (1GateCircStr <*x,y*>,'&' ) by Th43;
then A1: y in the carrier of ((1GateCircStr <*x,y*>,'&' ) +* (1GateCircStr <*y,c*>,'&' )) by Th20;
( x in the carrier of (1GateCircStr <*c,x*>,'&' ) & c in the carrier of (1GateCircStr <*c,x*>,'&' ) ) by Th43;
then ( x in the carrier of (MajorityIStr x,y,c) & y in the carrier of (MajorityIStr x,y,c) & c in the carrier of (MajorityIStr x,y,c) ) by A1, 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 Th20; :: thesis: verum