let x1, x2, x3, x5, x6, x7 be non pair set ; :: thesis: for s being State of (STC0IICirc (x1,x2,x3,x5,x6,x7)) holds Following (s,2) is stable
set S1 = BitGFA0Str (x1,x2,x3);
set S2 = BitGFA0Str (x5,x6,x7);
set C = STC0IICirc (x1,x2,x3,x5,x6,x7);
set C1 = BitGFA0Circ (x1,x2,x3);
set C2 = BitGFA0Circ (x5,x6,x7);
set n1 = 2;
set n2 = 2;
A1: ( InputVertices (BitGFA0Str (x1,x2,x3)) misses InnerVertices (BitGFA0Str (x5,x6,x7)) & InputVertices (BitGFA0Str (x5,x6,x7)) misses InnerVertices (BitGFA0Str (x1,x2,x3)) ) by LmSTC0IIS09a;
let s be State of (STC0IICirc (x1,x2,x3,x5,x6,x7)); :: thesis: Following (s,2) is stable
reconsider s1 = s | the carrier of (BitGFA0Str (x1,x2,x3)) as State of (BitGFA0Circ (x1,x2,x3)) by FACIRC_1:26;
reconsider s2 = s | the carrier of (BitGFA0Str (x5,x6,x7)) as State of (BitGFA0Circ (x5,x6,x7)) by FACIRC_1:26;
( Following (s1,2) is stable & Following (s2,2) is stable ) by GFACIRC1:40;
then Following (s,(max (2,2))) is stable by A1, CIRCCOMB:60, CIRCCMB2:22;
hence Following (s,2) is stable ; :: thesis: verum