let am, bp, cm be non pair set ; :: thesis: for x, y, z being set holds InputVertices (BitGFA2Str (am,bp,cm)) misses InnerVertices (BitGFA1Str (x,y,z))
let x, y, z be set ; :: thesis: InputVertices (BitGFA2Str (am,bp,cm)) misses InnerVertices (BitGFA1Str (x,y,z))
set S1 = BitGFA2Str (am,bp,cm);
InputVertices (BitGFA2Str (am,bp,cm)) is without_pairs by GFACIRC1:99;
hence InputVertices (BitGFA2Str (am,bp,cm)) misses InnerVertices (BitGFA1Str (x,y,z)) by FACIRC_1:5, GFACIRC1:64; :: thesis: verum