theorem Th111: :: GFACIRC1:111

for x, y, z being set holds
( x in the carrier of (GFA3CarryStr (x,y,z)) & y in the carrier of (GFA3CarryStr (x,y,z)) & z in the carrier of (GFA3CarryStr (x,y,z)) & [<*x,y*>,nor2] in the carrier of (GFA3CarryStr (x,y,z)) & [<*y,z*>,nor2] in the carrier of (GFA3CarryStr (x,y,z)) & [<*z,x*>,nor2] in the carrier of (GFA3CarryStr (x,y,z)) & [<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3] in the carrier of (GFA3CarryStr (x,y,z)) )