let x, y, z be set ; :: thesis: for p being set holds GFA3AdderOutput (x,y,z) <> [p,and2b]
let p be set ; :: thesis: GFA3AdderOutput (x,y,z) <> [p,and2b]
set A1 = GFA3AdderOutput (x,y,z);

now

assume [p,and2b] `2 = (GFA3AdderOutput (x,y,z)) `2 ; :: thesis: contradiction
then A1: [p,and2b] `2 = xor2 by MCART_1:7;
[p,and2b] `2 = and2b by MCART_1:7;
hence contradiction by A1, TWOSCOMP:11, TWOSCOMP:13; :: thesis: verum

end;

hence GFA3AdderOutput (x,y,z) <> [p,and2b] ; :: thesis: verum