let x, y, z be non pair set ; :: thesis: InputVertices (BitGFA3Str (x,y,z)) = {x,y,z}
set S = BitGFA3Str (x,y,z);
set S1 = GFA3AdderStr (x,y,z);
set S2 = GFA3CarryStr (x,y,z);
A1: ( InputVertices (GFA3AdderStr (x,y,z)) = {x,y,z} & InputVertices (GFA3CarryStr (x,y,z)) = {x,y,z} ) by Th114, FACIRC_1:57;
( InnerVertices (GFA3AdderStr (x,y,z)) is Relation & InnerVertices (GFA3CarryStr (x,y,z)) is Relation ) by Th107, FACIRC_1:58;
hence InputVertices (BitGFA3Str (x,y,z)) = {x,y,z} \/ {x,y,z} by A1, FACIRC_1:7
.= {x,y,z} ;
:: thesis: verum