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

now :: thesis: not [p,and2c] `2 = (GFA1AdderOutput (x,y,z)) `2

assume [p,and2c] `2 = (GFA1AdderOutput (x,y,z)) `2 ; :: thesis: contradiction
then A1: [p,and2c] `2 = xor2c by MCART_1:7;
thus contradiction by A1, GFACIRC1:3, GFACIRC1:4; :: thesis: verum

end;

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