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 f1 = and2b ;
set f2 = and2b ;
set f3 = and2b ;
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:6 ;
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