let ap, bm, cp be non pair set ; :: thesis: for x, y, z being set holds InputVertices (BitGFA1Str (ap,bm,cp)) misses InnerVertices (BitGFA2Str (x,y,z))
let x, y, z be set ; :: thesis: InputVertices (BitGFA1Str (ap,bm,cp)) misses InnerVertices (BitGFA2Str (x,y,z))
set S1 = BitGFA1Str (ap,bm,cp);
InputVertices (BitGFA1Str (ap,bm,cp)) is without_pairs by GFACIRC1:67;
hence InputVertices (BitGFA1Str (ap,bm,cp)) misses InnerVertices (BitGFA2Str (x,y,z)) by FACIRC_1:5, GFACIRC1:96; :: thesis: verum