set f1 = and2b ;
set f2 = and2b ;
set f3 = and2b ;
let x, y, z be set ; :: thesis: ( [<*x,y*>,and2b ] in InnerVertices (GFA3CarryStr x,y,z) & [<*y,z*>,and2b ] in InnerVertices (GFA3CarryStr x,y,z) & [<*z,x*>,and2b ] in InnerVertices (GFA3CarryStr x,y,z) & GFA3CarryOutput x,y,z in InnerVertices (GFA3CarryStr x,y,z) )
set xy = [<*x,y*>,and2b ];
set yz = [<*y,z*>,and2b ];
set zx = [<*z,x*>,and2b ];
InnerVertices (GFA3CarryStr x,y,z) = {[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]} \/ {(GFA3CarryOutput x,y,z)} by Th124
.= {[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ],(GFA3CarryOutput x,y,z)} by ENUMSET1:46 ;
hence ( [<*x,y*>,and2b ] in InnerVertices (GFA3CarryStr x,y,z) & [<*y,z*>,and2b ] in InnerVertices (GFA3CarryStr x,y,z) & [<*z,x*>,and2b ] in InnerVertices (GFA3CarryStr x,y,z) & GFA3CarryOutput x,y,z in InnerVertices (GFA3CarryStr x,y,z) ) by ENUMSET1:def 2; :: thesis: verum