:: deftheorem defines GFA0CarryOutput GFACIRC1:def 9 :
for x, y, z being set holds GFA0CarryOutput (x,y,z) = [<*[<*x,y*>,and2],[<*y,z*>,and2],[<*z,x*>,and2]*>,or3];