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