let ap, bp, cp be non pair set ; :: thesis: for x, y, z being set holds InputVertices (BitGFA0Str (ap,bp,cp)) misses InnerVertices (BitGFA0Str (x,y,z))
let x, y, z be set ; :: thesis: InputVertices (BitGFA0Str (ap,bp,cp)) misses InnerVertices (BitGFA0Str (x,y,z))
set S1 = BitGFA0Str (ap,bp,cp);
InputVertices (BitGFA0Str (ap,bp,cp)) is without_pairs by GFACIRC1:35;
hence InputVertices (BitGFA0Str (ap,bp,cp)) misses InnerVertices (BitGFA0Str (x,y,z)) by FACIRC_1:5, GFACIRC1:32; :: thesis: verum