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;
set S2 = BitGFA2Str x,y,z;
( not InputVertices (BitGFA1Str ap,bm,cp) is with_pair & InnerVertices (BitGFA2Str x,y,z) is Relation ) by GFACIRC1:80, GFACIRC1:114;
hence InputVertices (BitGFA1Str ap,bm,cp) misses InnerVertices (BitGFA2Str x,y,z) by FACIRC_1:5; :: thesis: verum