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;
set S2 = BitGFA3Str x,y,z;
not InputVertices (BitGFA3Str am,bm,cm) is with_pair by GFACIRC1:154;
hence InputVertices (BitGFA3Str am,bm,cm) misses InnerVertices (BitGFA3Str x,y,z) by FACIRC_1:5, GFACIRC1:151; :: thesis: verum