let x1, x2, x3, x5, x6, x7 be non pair set ; :: thesis: for a, b, c being set holds InputVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) misses InnerVertices (BitGFA0Str (a,b,c))
let a, b, c be set ; :: thesis: InputVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) misses InnerVertices (BitGFA0Str (a,b,c))
set S1 = STC0IIStr (x1,x2,x3,x5,x6,x7);
set S2 = BitGFA0Str (a,b,c);
( InputVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) is without_pairs & InnerVertices (BitGFA0Str (a,b,c)) is Relation ) by ThSTC0IIS5;
hence InputVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) misses InnerVertices (BitGFA0Str (a,b,c)) ; :: thesis: verum