let a, b, c be non pair set ; :: thesis: for x, y, z being set holds InputVertices (BitGFA0Str (a,b,c)) misses InnerVertices (BitGFA0Str (x,y,z))
let x, y, z be set ; :: thesis: InputVertices (BitGFA0Str (a,b,c)) misses InnerVertices (BitGFA0Str (x,y,z))
set S1 = BitGFA0Str (a,b,c);
set S2 = BitGFA0Str (x,y,z);
( InputVertices (BitGFA0Str (a,b,c)) is without_pairs & InnerVertices (BitGFA0Str (x,y,z)) is Relation ) by GFACIRC1:35;
hence InputVertices (BitGFA0Str (a,b,c)) misses InnerVertices (BitGFA0Str (x,y,z)) ; :: thesis: verum