let x, y, z be non pair set ; :: thesis: InputVertices (BitGFA1Str x,y,z) = {x,y,z}
set S = BitGFA1Str x,y,z;
set S1 = GFA1AdderStr x,y,z;
set S2 = GFA1CarryStr x,y,z;
A1: ( InputVertices (GFA1AdderStr x,y,z) = {x,y,z} & InputVertices (GFA1CarryStr x,y,z) = {x,y,z} ) by Th58, FACIRC_1:57;
( InnerVertices (GFA1AdderStr x,y,z) is Relation & InnerVertices (GFA1CarryStr x,y,z) is Relation ) by Th51, FACIRC_1:58;
hence InputVertices (BitGFA1Str x,y,z) = {x,y,z} \/ {x,y,z} by A1, FACIRC_1:7
.= {x,y,z} ;
:: thesis: verum