theorem Th24: :: FACIRC_2:24

for x, y being FinSequence
for n being Nat holds
( ( (n -BitMajorityOutput (x,y)) `1 = <*> & (n -BitMajorityOutput (x,y)) `2 = (0 -tuples_on BOOLEAN) --> FALSE & proj1 ((n -BitMajorityOutput (x,y)) `2) = 0 -tuples_on BOOLEAN ) or ( card ((n -BitMajorityOutput (x,y)) `1) = 3 & (n -BitMajorityOutput (x,y)) `2 = or3 & proj1 ((n -BitMajorityOutput (x,y)) `2) = 3 -tuples_on BOOLEAN ) )