let x1, x2, x3, x4, x5, x6, x7 be non pair set ; :: thesis: for C1, C2, C3 being set holds InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) misses InnerVertices (BitGFA0Str (C1,C2,C3))
let C1, C2, C3 be set ; :: thesis: InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) misses InnerVertices (BitGFA0Str (C1,C2,C3))
set S1 = STC0IStr (x1,x2,x3,x4,x5,x6,x7);
set S2 = BitGFA0Str (C1,C2,C3);
( InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) is without_pairs & InnerVertices (BitGFA0Str (C1,C2,C3)) is Relation ) by ThSTC0IS5;
hence InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) misses InnerVertices (BitGFA0Str (C1,C2,C3)) ; :: thesis: verum