theorem Th25: :: FACIRC_2:25

for n being Nat
for x, y being FinSequence
for p being set holds
( n -BitMajorityOutput (x,y) <> [p,'&'] & n -BitMajorityOutput (x,y) <> [p,'xor'] )