let x, b be non pair set ; :: thesis: InnerVertices (BitCompStr (x,b)) is Relation
set S1 = CompStr (x,b);
set S2 = IncrementStr (x,b);
( InnerVertices (CompStr (x,b)) is Relation & InnerVertices (IncrementStr (x,b)) is Relation ) by FACIRC_1:38;
hence InnerVertices (BitCompStr (x,b)) is Relation by FACIRC_1:3; :: thesis: verum