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