let am, bm, cm be non pair set ; :: thesis: for x, y, z being set holds InputVertices (BitGFA3Str (am,bm,cm)) misses InnerVertices (BitGFA3Str (x,y,z))
let x, y, z be set ; :: thesis: InputVertices (BitGFA3Str (am,bm,cm)) misses InnerVertices (BitGFA3Str (x,y,z))
set S1 = BitGFA3Str (am,bm,cm);
InputVertices (BitGFA3Str (am,bm,cm)) is without_pairs by GFACIRC1:131;
hence InputVertices (BitGFA3Str (am,bm,cm)) misses InnerVertices (BitGFA3Str (x,y,z)) by FACIRC_1:5, GFACIRC1:128; :: thesis: verum