let i, n be Nat; :: thesis: for o1 being TermOrder of (i + 1)
for o2 being TermOrder of (n -' (i + 1)) st o1 is admissible & o2 is admissible holds
BlockOrder (i,n,o1,o2) is admissible
let o1 be TermOrder of (i + 1); :: thesis: for o2 being TermOrder of (n -' (i + 1)) st o1 is admissible & o2 is admissible holds
BlockOrder (i,n,o1,o2) is admissible
let o2 be TermOrder of (n -' (i + 1)); :: thesis: ( o1 is admissible & o2 is admissible implies BlockOrder (i,n,o1,o2) is admissible )
assume that
A1: o1 is admissible and
A2: o2 is admissible ; :: thesis: BlockOrder (i,n,o1,o2) is admissible
A3: i + 1 = (i + 1) -' 0 by NAT_D:40;
then A4: o1 is_strongly_connected_in Bags ((i + 1) -' 0) by A1;
A5: o2 is_strongly_connected_in Bags (n -' (i + 1)) by A2;
set BO = BlockOrder (i,n,o1,o2);

now :: thesis: ( BlockOrder (i,n,o1,o2) is_strongly_connected_in Bags n & ( for a being bag of n holds
( [(EmptyBag n),a] in BlockOrder (i,n,o1,o2) & ( for a, b, c being bag of n st [a,b] in BlockOrder (i,n,o1,o2) holds
[(a + c),(b + c)] in BlockOrder (i,n,o1,o2) ) ) ) )

now :: thesis: for x, y being object st x in Bags n & y in Bags n & not [x,y] in BlockOrder (i,n,o1,o2) holds
[y,x] in BlockOrder (i,n,o1,o2)

let x, y be object ; :: thesis: ( x in Bags n & y in Bags n & not [x,y] in BlockOrder (i,n,o1,o2) implies [b₂,b₁] in BlockOrder (i,n,o1,o2) )
assume that
A6: x in Bags n and
A7: y in Bags n ; :: thesis: ( not [x,y] in BlockOrder (i,n,o1,o2) implies [b₂,b₁] in BlockOrder (i,n,o1,o2) )
reconsider p = x, q = y as bag of n by A6, A7;
set CUTP1 = (0,(i + 1)) -cut p;
set CUTP2 = ((i + 1),n) -cut p;
set CUTQ1 = (0,(i + 1)) -cut q;
set CUTQ2 = ((i + 1),n) -cut q;
A8: (0,(i + 1)) -cut p in Bags ((i + 1) -' 0) by PRE_POLY:def 12;
A9: (0,(i + 1)) -cut q in Bags ((i + 1) -' 0) by PRE_POLY:def 12;
A10: ((i + 1),n) -cut p in Bags (n -' (i + 1)) by PRE_POLY:def 12;
A11: ((i + 1),n) -cut q in Bags (n -' (i + 1)) by PRE_POLY:def 12;
assume A12: not [x,y] in BlockOrder (i,n,o1,o2) ; :: thesis: [b₂,b₁] in BlockOrder (i,n,o1,o2)

per cases ( (0,(i + 1)) -cut p = (0,(i + 1)) -cut q or not [((0,(i + 1)) -cut p),((0,(i + 1)) -cut q)] in o1 ) by A12, Def10;

suppose A13: (0,(i + 1)) -cut p = (0,(i + 1)) -cut q ; :: thesis: [b₂,b₁] in BlockOrder (i,n,o1,o2)

now :: thesis: [y,x] in BlockOrder (i,n,o1,o2)

per cases ( (0,(i + 1)) -cut p <> (0,(i + 1)) -cut q or not [(((i + 1),n) -cut p),(((i + 1),n) -cut q)] in o2 ) by A12, Def10;

suppose (0,(i + 1)) -cut p <> (0,(i + 1)) -cut q ; :: thesis: [y,x] in BlockOrder (i,n,o1,o2)

hence [y,x] in BlockOrder (i,n,o1,o2) by A13; :: thesis: verum

end;

suppose not [(((i + 1),n) -cut p),(((i + 1),n) -cut q)] in o2 ; :: thesis: [y,x] in BlockOrder (i,n,o1,o2)

then [(((i + 1),n) -cut q),(((i + 1),n) -cut p)] in o2 by A5, A10, A11;
hence [y,x] in BlockOrder (i,n,o1,o2) by A13, Def10; :: thesis: verum

end;

end;

end;

hence [y,x] in BlockOrder (i,n,o1,o2) ; :: thesis: verum

end;

suppose not [((0,(i + 1)) -cut p),((0,(i + 1)) -cut q)] in o1 ; :: thesis: [b₂,b₁] in BlockOrder (i,n,o1,o2)

then A14: [((0,(i + 1)) -cut q),((0,(i + 1)) -cut p)] in o1 by A4, A8, A9;

now :: thesis: [y,x] in BlockOrder (i,n,o1,o2)

per cases ( (0,(i + 1)) -cut p <> (0,(i + 1)) -cut q or not [(((i + 1),n) -cut p),(((i + 1),n) -cut q)] in o2 ) by A12, Def10;

suppose (0,(i + 1)) -cut p <> (0,(i + 1)) -cut q ; :: thesis: [y,x] in BlockOrder (i,n,o1,o2)

hence [y,x] in BlockOrder (i,n,o1,o2) by A14, Def10; :: thesis: verum

end;

suppose not [(((i + 1),n) -cut p),(((i + 1),n) -cut q)] in o2 ; :: thesis: [y,x] in BlockOrder (i,n,o1,o2)

then A15: [(((i + 1),n) -cut q),(((i + 1),n) -cut p)] in o2 by A5, A10, A11;

per cases ( (0,(i + 1)) -cut p = (0,(i + 1)) -cut q or (0,(i + 1)) -cut p <> (0,(i + 1)) -cut q ) ;

suppose (0,(i + 1)) -cut p = (0,(i + 1)) -cut q ; :: thesis: [y,x] in BlockOrder (i,n,o1,o2)

hence [y,x] in BlockOrder (i,n,o1,o2) by A15, Def10; :: thesis: verum

end;

suppose (0,(i + 1)) -cut p <> (0,(i + 1)) -cut q ; :: thesis: [y,x] in BlockOrder (i,n,o1,o2)

hence [y,x] in BlockOrder (i,n,o1,o2) by A14, Def10; :: thesis: verum

end;

end;

end;

end;

end;

hence [y,x] in BlockOrder (i,n,o1,o2) ; :: thesis: verum

end;

end;

end;

hence BlockOrder (i,n,o1,o2) is_strongly_connected_in Bags n ; :: thesis: for a being bag of n holds
( [(EmptyBag n),a] in BlockOrder (i,n,o1,o2) & ( for a, b, c being bag of n st [a,b] in BlockOrder (i,n,o1,o2) holds
[(b₆ + b₈),(b₇ + b₈)] in BlockOrder (i,n,o1,o2) ) )
let a be bag of n; :: thesis: ( [(EmptyBag n),a] in BlockOrder (i,n,o1,o2) & ( for a, b, c being bag of n st [a,b] in BlockOrder (i,n,o1,o2) holds
[(b₅ + b₇),(b₆ + b₇)] in BlockOrder (i,n,o1,o2) ) )
set CUTE1 = (0,(i + 1)) -cut (EmptyBag n);
set CUTA1 = (0,(i + 1)) -cut a;
set CUTE2 = ((i + 1),n) -cut (EmptyBag n);
set CUTA2 = ((i + 1),n) -cut a;

now :: thesis: [(EmptyBag n),a] in BlockOrder (i,n,o1,o2)

per cases ( (0,(i + 1)) -cut (EmptyBag n) <> (0,(i + 1)) -cut a or (0,(i + 1)) -cut (EmptyBag n) = (0,(i + 1)) -cut a ) ;

suppose A16: (0,(i + 1)) -cut (EmptyBag n) <> (0,(i + 1)) -cut a ; :: thesis: [(EmptyBag n),a] in BlockOrder (i,n,o1,o2)

(0,(i + 1)) -cut (EmptyBag n) = EmptyBag ((i + 1) -' 0) by Th15;
then [((0,(i + 1)) -cut (EmptyBag n)),((0,(i + 1)) -cut a)] in o1 by A1, A3;
hence [(EmptyBag n),a] in BlockOrder (i,n,o1,o2) by A16, Def10; :: thesis: verum

end;

suppose A17: (0,(i + 1)) -cut (EmptyBag n) = (0,(i + 1)) -cut a ; :: thesis: [(EmptyBag n),a] in BlockOrder (i,n,o1,o2)

((i + 1),n) -cut (EmptyBag n) = EmptyBag (n -' (i + 1)) by Th15;
then [(((i + 1),n) -cut (EmptyBag n)),(((i + 1),n) -cut a)] in o2 by A2;
hence [(EmptyBag n),a] in BlockOrder (i,n,o1,o2) by A17, Def10; :: thesis: verum

end;

end;

end;

hence [(EmptyBag n),a] in BlockOrder (i,n,o1,o2) ; :: thesis: for a, b, c being bag of n st [a,b] in BlockOrder (i,n,o1,o2) holds
[(b₅ + b₇),(b₆ + b₇)] in BlockOrder (i,n,o1,o2)
let a, b, c be bag of n; :: thesis: ( [a,b] in BlockOrder (i,n,o1,o2) implies [(b₂ + b₄),(b₃ + b₄)] in BlockOrder (i,n,o1,o2) )
assume A18: [a,b] in BlockOrder (i,n,o1,o2) ; :: thesis: [(b₂ + b₄),(b₃ + b₄)] in BlockOrder (i,n,o1,o2)
set CUTA1 = (0,(i + 1)) -cut a;
set CUTA2 = ((i + 1),n) -cut a;
set CUTB1 = (0,(i + 1)) -cut b;
set CUTB2 = ((i + 1),n) -cut b;
set CUTC1 = (0,(i + 1)) -cut c;
set CUTC2 = ((i + 1),n) -cut c;
set CUTAC1 = (0,(i + 1)) -cut (a + c);
set CUTBC1 = (0,(i + 1)) -cut (b + c);
set CUTAC2 = ((i + 1),n) -cut (a + c);
set CUTBC2 = ((i + 1),n) -cut (b + c);

per cases ( ( (0,(i + 1)) -cut a <> (0,(i + 1)) -cut b & [((0,(i + 1)) -cut a),((0,(i + 1)) -cut b)] in o1 ) or ( (0,(i + 1)) -cut a = (0,(i + 1)) -cut b & [(((i + 1),n) -cut a),(((i + 1),n) -cut b)] in o2 ) ) by A18, Def10;

suppose A19: ( (0,(i + 1)) -cut a <> (0,(i + 1)) -cut b & [((0,(i + 1)) -cut a),((0,(i + 1)) -cut b)] in o1 ) ; :: thesis: [(b₂ + b₄),(b₃ + b₄)] in BlockOrder (i,n,o1,o2)

then [(((0,(i + 1)) -cut a) + ((0,(i + 1)) -cut c)),(((0,(i + 1)) -cut b) + ((0,(i + 1)) -cut c))] in o1 by A1, A3;
then [((0,(i + 1)) -cut (a + c)),(((0,(i + 1)) -cut b) + ((0,(i + 1)) -cut c))] in o1 by Th16;
then A20: [((0,(i + 1)) -cut (a + c)),((0,(i + 1)) -cut (b + c))] in o1 by Th16;

now :: thesis: not ((0,(i + 1)) -cut a) + ((0,(i + 1)) -cut c) = ((0,(i + 1)) -cut b) + ((0,(i + 1)) -cut c)

assume A21: ((0,(i + 1)) -cut a) + ((0,(i + 1)) -cut c) = ((0,(i + 1)) -cut b) + ((0,(i + 1)) -cut c) ; :: thesis: contradiction
(((0,(i + 1)) -cut a) + ((0,(i + 1)) -cut c)) -' ((0,(i + 1)) -cut c) = (0,(i + 1)) -cut a by PRE_POLY:48;
hence contradiction by A19, A21, PRE_POLY:48; :: thesis: verum

end;

then (0,(i + 1)) -cut (a + c) <> ((0,(i + 1)) -cut b) + ((0,(i + 1)) -cut c) by Th16;
then (0,(i + 1)) -cut (a + c) <> (0,(i + 1)) -cut (b + c) by Th16;
hence [(a + c),(b + c)] in BlockOrder (i,n,o1,o2) by A20, Def10; :: thesis: verum

end;

suppose A22: ( (0,(i + 1)) -cut a = (0,(i + 1)) -cut b & [(((i + 1),n) -cut a),(((i + 1),n) -cut b)] in o2 ) ; :: thesis: [(b₂ + b₄),(b₃ + b₄)] in BlockOrder (i,n,o1,o2)

then [((((i + 1),n) -cut a) + (((i + 1),n) -cut c)),((((i + 1),n) -cut b) + (((i + 1),n) -cut c))] in o2 by A2;
then [(((i + 1),n) -cut (a + c)),((((i + 1),n) -cut b) + (((i + 1),n) -cut c))] in o2 by Th16;
then A23: [(((i + 1),n) -cut (a + c)),(((i + 1),n) -cut (b + c))] in o2 by Th16;
(0,(i + 1)) -cut (a + c) = ((0,(i + 1)) -cut b) + ((0,(i + 1)) -cut c) by A22, Th16;
then (0,(i + 1)) -cut (a + c) = (0,(i + 1)) -cut (b + c) by Th16;
hence [(a + c),(b + c)] in BlockOrder (i,n,o1,o2) by A23, Def10; :: thesis: verum

end;

end;

end;

hence BlockOrder (i,n,o1,o2) is admissible ; :: thesis: verum