:: MCART_6 semantic presentation

theorem Th1: :: MCART_6:1
for b1 being set st b1 <> {} holds
ex b2 being set st
( b2 in b1 & ( for b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16 being set st b3 in b4 & b4 in b5 & b5 in b6 & b6 in b7 & b7 in b8 & b8 in b9 & b9 in b10 & b10 in b11 & b11 in b12 & b12 in b13 & b13 in b14 & b14 in b15 & b15 in b16 & b16 in b2 holds
b3 misses b1 ) )
proof end;

theorem Th2: :: MCART_6:2
for b1 being set st b1 <> {} holds
ex b2 being set st
( b2 in b1 & ( for b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17 being set st b3 in b4 & b4 in b5 & b5 in b6 & b6 in b7 & b7 in b8 & b8 in b9 & b9 in b10 & b10 in b11 & b11 in b12 & b12 in b13 & b13 in b14 & b14 in b15 & b15 in b16 & b16 in b17 & b17 in b2 holds
b3 misses b1 ) )
proof end;

definition
let c1, c2, c3, c4, c5, c6, c7, c8, c9 be set ;
func [c1,c2,c3,c4,c5,c6,c7,c8,c9] -> set equals :: MCART_6:def 1
[[a1,a2,a3,a4,a5,a6,a7,a8],a9];
coherence
[[c1,c2,c3,c4,c5,c6,c7,c8],c9] is set ;
end;

:: deftheorem Def1 defines [ MCART_6:def 1 :
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds [b1,b2,b3,b4,b5,b6,b7,b8,b9] = [[b1,b2,b3,b4,b5,b6,b7,b8],b9];

theorem Th3: :: MCART_6:3
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds [b1,b2,b3,b4,b5,b6,b7,b8,b9] = [[[[[[[[b1,b2],b3],b4],b5],b6],b7],b8],b9]
proof end;

theorem Th4: :: MCART_6:4
canceled;

theorem Th5: :: MCART_6:5
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds [b1,b2,b3,b4,b5,b6,b7,b8,b9] = [[b1,b2,b3,b4,b5,b6,b7],b8,b9]
proof end;

theorem Th6: :: MCART_6:6
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds [b1,b2,b3,b4,b5,b6,b7,b8,b9] = [[b1,b2,b3,b4,b5,b6],b7,b8,b9]
proof end;

theorem Th7: :: MCART_6:7
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds [b1,b2,b3,b4,b5,b6,b7,b8,b9] = [[b1,b2,b3,b4,b5],b6,b7,b8,b9]
proof end;

theorem Th8: :: MCART_6:8
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds [b1,b2,b3,b4,b5,b6,b7,b8,b9] = [[b1,b2,b3,b4],b5,b6,b7,b8,b9]
proof end;

theorem Th9: :: MCART_6:9
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds [b1,b2,b3,b4,b5,b6,b7,b8,b9] = [[b1,b2,b3],b4,b5,b6,b7,b8,b9]
proof end;

theorem Th10: :: MCART_6:10
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds [b1,b2,b3,b4,b5,b6,b7,b8,b9] = [[b1,b2],b3,b4,b5,b6,b7,b8,b9]
proof end;

theorem Th11: :: MCART_6:11
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18 being set st [b1,b2,b3,b4,b5,b6,b7,b8,b9] = [b10,b11,b12,b13,b14,b15,b16,b17,b18] holds
( b1 = b10 & b2 = b11 & b3 = b12 & b4 = b13 & b5 = b14 & b6 = b15 & b7 = b16 & b8 = b17 & b9 = b18 )
proof end;

definition
let c1, c2, c3, c4, c5, c6, c7, c8, c9 be set ;
func [:c1,c2,c3,c4,c5,c6,c7,c8,c9:] -> set equals :: MCART_6:def 2
[:[:a1,a2,a3,a4,a5,a6,a7,a8:],a9:];
coherence
[:[:c1,c2,c3,c4,c5,c6,c7,c8:],c9:] is set ;
end;

:: deftheorem Def2 defines [: MCART_6:def 2 :
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] = [:[:b1,b2,b3,b4,b5,b6,b7,b8:],b9:];

theorem Th12: :: MCART_6:12
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] = [:[:[:[:[:[:[:[:b1,b2:],b3:],b4:],b5:],b6:],b7:],b8:],b9:]
proof end;

theorem Th13: :: MCART_6:13
canceled;

theorem Th14: :: MCART_6:14
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] = [:[:b1,b2,b3,b4,b5,b6,b7:],b8,b9:]
proof end;

theorem Th15: :: MCART_6:15
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] = [:[:b1,b2,b3,b4,b5,b6:],b7,b8,b9:]
proof end;

theorem Th16: :: MCART_6:16
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] = [:[:b1,b2,b3,b4,b5:],b6,b7,b8,b9:]
proof end;

theorem Th17: :: MCART_6:17
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] = [:[:b1,b2,b3,b4:],b5,b6,b7,b8,b9:]
proof end;

theorem Th18: :: MCART_6:18
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] = [:[:b1,b2,b3:],b4,b5,b6,b7,b8,b9:]
proof end;

theorem Th19: :: MCART_6:19
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] = [:[:b1,b2:],b3,b4,b5,b6,b7,b8,b9:]
proof end;

theorem Th20: :: MCART_6:20
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds
( ( b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} ) iff [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] <> {} )
proof end;

theorem Th21: :: MCART_6:21
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18 being set st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} & [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] = [:b10,b11,b12,b13,b14,b15,b16,b17,b18:] holds
( b1 = b10 & b2 = b11 & b3 = b12 & b4 = b13 & b5 = b14 & b6 = b15 & b7 = b16 & b8 = b17 & b9 = b18 )
proof end;

theorem Th22: :: MCART_6:22
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18 being set st [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] <> {} & [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] = [:b10,b11,b12,b13,b14,b15,b16,b17,b18:] holds
( b1 = b10 & b2 = b11 & b3 = b12 & b4 = b13 & b5 = b14 & b6 = b15 & b7 = b16 & b8 = b17 & b9 = b18 )
proof end;

theorem Th23: :: MCART_6:23
for b1, b2 being set st [:b1,b1,b1,b1,b1,b1,b1,b1,b1:] = [:b2,b2,b2,b2,b2,b2,b2,b2,b2:] holds
b1 = b2
proof end;

theorem Th24: :: MCART_6:24
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} holds
for b10 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] ex b11 being Element of b1ex b12 being Element of b2ex b13 being Element of b3ex b14 being Element of b4ex b15 being Element of b5ex b16 being Element of b6ex b17 being Element of b7ex b18 being Element of b8ex b19 being Element of b9 st b10 = [b11,b12,b13,b14,b15,b16,b17,b18,b19]
proof end;

definition
let c1, c2, c3, c4, c5, c6, c7, c8, c9 be set ;
assume E9: ( c1 <> {} & c2 <> {} & c3 <> {} & c4 <> {} & c5 <> {} & c6 <> {} & c7 <> {} & c8 <> {} & c9 <> {} ) ;
let c10 be Element of [:c1,c2,c3,c4,c5,c6,c7,c8,c9:];
func c10 `1 -> Element of a1 means :Def3: :: MCART_6:def 3
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st a10 = [b1,b2,b3,b4,b5,b6,b7,b8,b9] holds
a11 = b1;
existence
ex b1 being Element of c1 st
for b2, b3, b4, b5, b6, b7, b8, b9, b10 being set st c10 = [b2,b3,b4,b5,b6,b7,b8,b9,b10] holds
b1 = b2
proof end;
uniqueness
for b1, b2 being Element of c1 st ( for b3, b4, b5, b6, b7, b8, b9, b10, b11 being set st c10 = [b3,b4,b5,b6,b7,b8,b9,b10,b11] holds
b1 = b3 ) & ( for b3, b4, b5, b6, b7, b8, b9, b10, b11 being set st c10 = [b3,b4,b5,b6,b7,b8,b9,b10,b11] holds
b2 = b3 ) holds
b1 = b2
proof end;
func c10 `2 -> Element of a2 means :Def4: :: MCART_6:def 4
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st a10 = [b1,b2,b3,b4,b5,b6,b7,b8,b9] holds
a11 = b2;
existence
ex b1 being Element of c2 st
for b2, b3, b4, b5, b6, b7, b8, b9, b10 being set st c10 = [b2,b3,b4,b5,b6,b7,b8,b9,b10] holds
b1 = b3
proof end;
uniqueness
for b1, b2 being Element of c2 st ( for b3, b4, b5, b6, b7, b8, b9, b10, b11 being set st c10 = [b3,b4,b5,b6,b7,b8,b9,b10,b11] holds
b1 = b4 ) & ( for b3, b4, b5, b6, b7, b8, b9, b10, b11 being set st c10 = [b3,b4,b5,b6,b7,b8,b9,b10,b11] holds
b2 = b4 ) holds
b1 = b2
proof end;
func c10 `3 -> Element of a3 means :Def5: :: MCART_6:def 5
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st a10 = [b1,b2,b3,b4,b5,b6,b7,b8,b9] holds
a11 = b3;
existence
ex b1 being Element of c3 st
for b2, b3, b4, b5, b6, b7, b8, b9, b10 being set st c10 = [b2,b3,b4,b5,b6,b7,b8,b9,b10] holds
b1 = b4
proof end;
uniqueness
for b1, b2 being Element of c3 st ( for b3, b4, b5, b6, b7, b8, b9, b10, b11 being set st c10 = [b3,b4,b5,b6,b7,b8,b9,b10,b11] holds
b1 = b5 ) & ( for b3, b4, b5, b6, b7, b8, b9, b10, b11 being set st c10 = [b3,b4,b5,b6,b7,b8,b9,b10,b11] holds
b2 = b5 ) holds
b1 = b2
proof end;
func c10 `4 -> Element of a4 means :Def6: :: MCART_6:def 6
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st a10 = [b1,b2,b3,b4,b5,b6,b7,b8,b9] holds
a11 = b4;
existence
ex b1 being Element of c4 st
for b2, b3, b4, b5, b6, b7, b8, b9, b10 being set st c10 = [b2,b3,b4,b5,b6,b7,b8,b9,b10] holds
b1 = b5
proof end;
uniqueness
for b1, b2 being Element of c4 st ( for b3, b4, b5, b6, b7, b8, b9, b10, b11 being set st c10 = [b3,b4,b5,b6,b7,b8,b9,b10,b11] holds
b1 = b6 ) & ( for b3, b4, b5, b6, b7, b8, b9, b10, b11 being set st c10 = [b3,b4,b5,b6,b7,b8,b9,b10,b11] holds
b2 = b6 ) holds
b1 = b2
proof end;
func c10 `5 -> Element of a5 means :Def7: :: MCART_6:def 7
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st a10 = [b1,b2,b3,b4,b5,b6,b7,b8,b9] holds
a11 = b5;
existence
ex b1 being Element of c5 st
for b2, b3, b4, b5, b6, b7, b8, b9, b10 being set st c10 = [b2,b3,b4,b5,b6,b7,b8,b9,b10] holds
b1 = b6
proof end;
uniqueness
for b1, b2 being Element of c5 st ( for b3, b4, b5, b6, b7, b8, b9, b10, b11 being set st c10 = [b3,b4,b5,b6,b7,b8,b9,b10,b11] holds
b1 = b7 ) & ( for b3, b4, b5, b6, b7, b8, b9, b10, b11 being set st c10 = [b3,b4,b5,b6,b7,b8,b9,b10,b11] holds
b2 = b7 ) holds
b1 = b2
proof end;
func c10 `6 -> Element of a6 means :Def8: :: MCART_6:def 8
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st a10 = [b1,b2,b3,b4,b5,b6,b7,b8,b9] holds
a11 = b6;
existence
ex b1 being Element of c6 st
for b2, b3, b4, b5, b6, b7, b8, b9, b10 being set st c10 = [b2,b3,b4,b5,b6,b7,b8,b9,b10] holds
b1 = b7
proof end;
uniqueness
for b1, b2 being Element of c6 st ( for b3, b4, b5, b6, b7, b8, b9, b10, b11 being set st c10 = [b3,b4,b5,b6,b7,b8,b9,b10,b11] holds
b1 = b8 ) & ( for b3, b4, b5, b6, b7, b8, b9, b10, b11 being set st c10 = [b3,b4,b5,b6,b7,b8,b9,b10,b11] holds
b2 = b8 ) holds
b1 = b2
proof end;
func c10 `7 -> Element of a7 means :Def9: :: MCART_6:def 9
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st a10 = [b1,b2,b3,b4,b5,b6,b7,b8,b9] holds
a11 = b7;
existence
ex b1 being Element of c7 st
for b2, b3, b4, b5, b6, b7, b8, b9, b10 being set st c10 = [b2,b3,b4,b5,b6,b7,b8,b9,b10] holds
b1 = b8
proof end;
uniqueness
for b1, b2 being Element of c7 st ( for b3, b4, b5, b6, b7, b8, b9, b10, b11 being set st c10 = [b3,b4,b5,b6,b7,b8,b9,b10,b11] holds
b1 = b9 ) & ( for b3, b4, b5, b6, b7, b8, b9, b10, b11 being set st c10 = [b3,b4,b5,b6,b7,b8,b9,b10,b11] holds
b2 = b9 ) holds
b1 = b2
proof end;
func c10 `8 -> Element of a8 means :Def10: :: MCART_6:def 10
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st a10 = [b1,b2,b3,b4,b5,b6,b7,b8,b9] holds
a11 = b8;
existence
ex b1 being Element of c8 st
for b2, b3, b4, b5, b6, b7, b8, b9, b10 being set st c10 = [b2,b3,b4,b5,b6,b7,b8,b9,b10] holds
b1 = b9
proof end;
uniqueness
for b1, b2 being Element of c8 st ( for b3, b4, b5, b6, b7, b8, b9, b10, b11 being set st c10 = [b3,b4,b5,b6,b7,b8,b9,b10,b11] holds
b1 = b10 ) & ( for b3, b4, b5, b6, b7, b8, b9, b10, b11 being set st c10 = [b3,b4,b5,b6,b7,b8,b9,b10,b11] holds
b2 = b10 ) holds
b1 = b2
proof end;
func c10 `9 -> Element of a9 means :Def11: :: MCART_6:def 11
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st a10 = [b1,b2,b3,b4,b5,b6,b7,b8,b9] holds
a11 = b9;
existence
ex b1 being Element of c9 st
for b2, b3, b4, b5, b6, b7, b8, b9, b10 being set st c10 = [b2,b3,b4,b5,b6,b7,b8,b9,b10] holds
b1 = b10
proof end;
uniqueness
for b1, b2 being Element of c9 st ( for b3, b4, b5, b6, b7, b8, b9, b10, b11 being set st c10 = [b3,b4,b5,b6,b7,b8,b9,b10,b11] holds
b1 = b11 ) & ( for b3, b4, b5, b6, b7, b8, b9, b10, b11 being set st c10 = [b3,b4,b5,b6,b7,b8,b9,b10,b11] holds
b2 = b11 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines `1 MCART_6:def 3 :
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} holds
for b10 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:]
for b11 being Element of b1 holds
( b11 = b10 `1 iff for b12, b13, b14, b15, b16, b17, b18, b19, b20 being set st b10 = [b12,b13,b14,b15,b16,b17,b18,b19,b20] holds
b11 = b12 );

:: deftheorem Def4 defines `2 MCART_6:def 4 :
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} holds
for b10 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:]
for b11 being Element of b2 holds
( b11 = b10 `2 iff for b12, b13, b14, b15, b16, b17, b18, b19, b20 being set st b10 = [b12,b13,b14,b15,b16,b17,b18,b19,b20] holds
b11 = b13 );

:: deftheorem Def5 defines `3 MCART_6:def 5 :
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} holds
for b10 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:]
for b11 being Element of b3 holds
( b11 = b10 `3 iff for b12, b13, b14, b15, b16, b17, b18, b19, b20 being set st b10 = [b12,b13,b14,b15,b16,b17,b18,b19,b20] holds
b11 = b14 );

:: deftheorem Def6 defines `4 MCART_6:def 6 :
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} holds
for b10 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:]
for b11 being Element of b4 holds
( b11 = b10 `4 iff for b12, b13, b14, b15, b16, b17, b18, b19, b20 being set st b10 = [b12,b13,b14,b15,b16,b17,b18,b19,b20] holds
b11 = b15 );

:: deftheorem Def7 defines `5 MCART_6:def 7 :
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} holds
for b10 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:]
for b11 being Element of b5 holds
( b11 = b10 `5 iff for b12, b13, b14, b15, b16, b17, b18, b19, b20 being set st b10 = [b12,b13,b14,b15,b16,b17,b18,b19,b20] holds
b11 = b16 );

:: deftheorem Def8 defines `6 MCART_6:def 8 :
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} holds
for b10 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:]
for b11 being Element of b6 holds
( b11 = b10 `6 iff for b12, b13, b14, b15, b16, b17, b18, b19, b20 being set st b10 = [b12,b13,b14,b15,b16,b17,b18,b19,b20] holds
b11 = b17 );

:: deftheorem Def9 defines `7 MCART_6:def 9 :
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} holds
for b10 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:]
for b11 being Element of b7 holds
( b11 = b10 `7 iff for b12, b13, b14, b15, b16, b17, b18, b19, b20 being set st b10 = [b12,b13,b14,b15,b16,b17,b18,b19,b20] holds
b11 = b18 );

:: deftheorem Def10 defines `8 MCART_6:def 10 :
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} holds
for b10 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:]
for b11 being Element of b8 holds
( b11 = b10 `8 iff for b12, b13, b14, b15, b16, b17, b18, b19, b20 being set st b10 = [b12,b13,b14,b15,b16,b17,b18,b19,b20] holds
b11 = b19 );

:: deftheorem Def11 defines `9 MCART_6:def 11 :
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} holds
for b10 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:]
for b11 being Element of b9 holds
( b11 = b10 `9 iff for b12, b13, b14, b15, b16, b17, b18, b19, b20 being set st b10 = [b12,b13,b14,b15,b16,b17,b18,b19,b20] holds
b11 = b20 );

theorem Th25: :: MCART_6:25
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} holds
for b10 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:]
for b11, b12, b13, b14, b15, b16, b17, b18, b19 being set st b10 = [b11,b12,b13,b14,b15,b16,b17,b18,b19] holds
( b10 `1 = b11 & b10 `2 = b12 & b10 `3 = b13 & b10 `4 = b14 & b10 `5 = b15 & b10 `6 = b16 & b10 `7 = b17 & b10 `8 = b18 & b10 `9 = b19 ) by Def3, Def4, Def5, Def6, Def7, Def8, Def9, Def10, Def11;

theorem Th26: :: MCART_6:26
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} holds
for b10 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] holds b10 = [(b10 `1 ),(b10 `2 ),(b10 `3 ),(b10 `4 ),(b10 `5 ),(b10 `6 ),(b10 `7 ),(b10 `8 ),(b10 `9 )]
proof end;

theorem Th27: :: MCART_6:27
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} holds
for b10 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] holds
( b10 `1 = (((((((b10 `1 ) `1 ) `1 ) `1 ) `1 ) `1 ) `1 ) `1 & b10 `2 = (((((((b10 `1 ) `1 ) `1 ) `1 ) `1 ) `1 ) `1 ) `2 & b10 `3 = ((((((b10 `1 ) `1 ) `1 ) `1 ) `1 ) `1 ) `2 & b10 `4 = (((((b10 `1 ) `1 ) `1 ) `1 ) `1 ) `2 & b10 `5 = ((((b10 `1 ) `1 ) `1 ) `1 ) `2 & b10 `6 = (((b10 `1 ) `1 ) `1 ) `2 & b10 `7 = ((b10 `1 ) `1 ) `2 & b10 `8 = (b10 `1 ) `2 & b10 `9 = b10 `2 )
proof end;

theorem Th28: :: MCART_6:28
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18 being set st [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] meets [:b10,b11,b12,b13,b14,b15,b16,b17,b18:] holds
( b1 meets b10 & b2 meets b11 & b3 meets b12 & b4 meets b13 & b5 meets b14 & b6 meets b15 & b7 meets b16 & b8 meets b17 & b9 meets b18 )
proof end;

theorem Th29: :: MCART_6:29
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds [:{b1},{b2},{b3},{b4},{b5},{b6},{b7},{b8},{b9}:] = {[b1,b2,b3,b4,b5,b6,b7,b8,b9]}
proof end;

theorem Th30: :: MCART_6:30
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set
for b10 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} holds
for b11, b12, b13, b14, b15, b16, b17, b18, b19 being set st b10 = [b11,b12,b13,b14,b15,b16,b17,b18,b19] holds
( b10 `1 = b11 & b10 `2 = b12 & b10 `3 = b13 & b10 `4 = b14 & b10 `5 = b15 & b10 `6 = b16 & b10 `7 = b17 & b10 `8 = b18 & b10 `9 = b19 ) by Def3, Def4, Def5, Def6, Def7, Def8, Def9, Def10, Def11;

theorem Th31: :: MCART_6:31
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10 being set
for b11 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} & ( for b12 being Element of b1
for b13 being Element of b2
for b14 being Element of b3
for b15 being Element of b4
for b16 being Element of b5
for b17 being Element of b6
for b18 being Element of b7
for b19 being Element of b8
for b20 being Element of b9 st b11 = [b12,b13,b14,b15,b16,b17,b18,b19,b20] holds
b10 = b12 ) holds
b10 = b11 `1
proof end;

theorem Th32: :: MCART_6:32
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10 being set
for b11 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} & ( for b12 being Element of b1
for b13 being Element of b2
for b14 being Element of b3
for b15 being Element of b4
for b16 being Element of b5
for b17 being Element of b6
for b18 being Element of b7
for b19 being Element of b8
for b20 being Element of b9 st b11 = [b12,b13,b14,b15,b16,b17,b18,b19,b20] holds
b10 = b13 ) holds
b10 = b11 `2
proof end;

theorem Th33: :: MCART_6:33
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10 being set
for b11 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} & ( for b12 being Element of b1
for b13 being Element of b2
for b14 being Element of b3
for b15 being Element of b4
for b16 being Element of b5
for b17 being Element of b6
for b18 being Element of b7
for b19 being Element of b8
for b20 being Element of b9 st b11 = [b12,b13,b14,b15,b16,b17,b18,b19,b20] holds
b10 = b14 ) holds
b10 = b11 `3
proof end;

theorem Th34: :: MCART_6:34
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10 being set
for b11 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} & ( for b12 being Element of b1
for b13 being Element of b2
for b14 being Element of b3
for b15 being Element of b4
for b16 being Element of b5
for b17 being Element of b6
for b18 being Element of b7
for b19 being Element of b8
for b20 being Element of b9 st b11 = [b12,b13,b14,b15,b16,b17,b18,b19,b20] holds
b10 = b15 ) holds
b10 = b11 `4
proof end;

theorem Th35: :: MCART_6:35
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10 being set
for b11 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} & ( for b12 being Element of b1
for b13 being Element of b2
for b14 being Element of b3
for b15 being Element of b4
for b16 being Element of b5
for b17 being Element of b6
for b18 being Element of b7
for b19 being Element of b8
for b20 being Element of b9 st b11 = [b12,b13,b14,b15,b16,b17,b18,b19,b20] holds
b10 = b16 ) holds
b10 = b11 `5
proof end;

theorem Th36: :: MCART_6:36
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10 being set
for b11 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} & ( for b12 being Element of b1
for b13 being Element of b2
for b14 being Element of b3
for b15 being Element of b4
for b16 being Element of b5
for b17 being Element of b6
for b18 being Element of b7
for b19 being Element of b8
for b20 being Element of b9 st b11 = [b12,b13,b14,b15,b16,b17,b18,b19,b20] holds
b10 = b17 ) holds
b10 = b11 `6
proof end;

theorem Th37: :: MCART_6:37
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10 being set
for b11 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} & ( for b12 being Element of b1
for b13 being Element of b2
for b14 being Element of b3
for b15 being Element of b4
for b16 being Element of b5
for b17 being Element of b6
for b18 being Element of b7
for b19 being Element of b8
for b20 being Element of b9 st b11 = [b12,b13,b14,b15,b16,b17,b18,b19,b20] holds
b10 = b18 ) holds
b10 = b11 `7
proof end;

theorem Th38: :: MCART_6:38
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10 being set
for b11 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} & ( for b12 being Element of b1
for b13 being Element of b2
for b14 being Element of b3
for b15 being Element of b4
for b16 being Element of b5
for b17 being Element of b6
for b18 being Element of b7
for b19 being Element of b8
for b20 being Element of b9 st b11 = [b12,b13,b14,b15,b16,b17,b18,b19,b20] holds
b10 = b19 ) holds
b10 = b11 `8
proof end;

theorem Th39: :: MCART_6:39
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10 being set
for b11 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} & ( for b12 being Element of b1
for b13 being Element of b2
for b14 being Element of b3
for b15 being Element of b4
for b16 being Element of b5
for b17 being Element of b6
for b18 being Element of b7
for b19 being Element of b8
for b20 being Element of b9 st b11 = [b12,b13,b14,b15,b16,b17,b18,b19,b20] holds
b10 = b20 ) holds
b10 = b11 `9
proof end;

theorem Th40: :: MCART_6:40
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10 being set st b1 in [:b2,b3,b4,b5,b6,b7,b8,b9,b10:] holds
ex b11, b12, b13, b14, b15, b16, b17, b18, b19 being set st
( b11 in b2 & b12 in b3 & b13 in b4 & b14 in b5 & b15 in b6 & b16 in b7 & b17 in b8 & b18 in b9 & b19 in b10 & b1 = [b11,b12,b13,b14,b15,b16,b17,b18,b19] )
proof end;

theorem Th41: :: MCART_6:41
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18 being set holds
( [b1,b2,b3,b4,b5,b6,b7,b8,b9] in [:b10,b11,b12,b13,b14,b15,b16,b17,b18:] iff ( b1 in b10 & b2 in b11 & b3 in b12 & b4 in b13 & b5 in b14 & b6 in b15 & b7 in b16 & b8 in b17 & b9 in b18 ) )
proof end;

theorem Th42: :: MCART_6:42
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10 being set st ( for b11 being set holds
( b11 in b1 iff ex b12, b13, b14, b15, b16, b17, b18, b19, b20 being set st
( b12 in b2 & b13 in b3 & b14 in b4 & b15 in b5 & b16 in b6 & b17 in b7 & b18 in b8 & b19 in b9 & b20 in b10 & b11 = [b12,b13,b14,b15,b16,b17,b18,b19,b20] ) ) ) holds
b1 = [:b2,b3,b4,b5,b6,b7,b8,b9,b10:]
proof end;

theorem Th43: :: MCART_6:43
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18 being set st b1 <> {} & b2 <> {} & b3 <> {} & b4 <> {} & b5 <> {} & b6 <> {} & b7 <> {} & b8 <> {} & b9 <> {} & b10 <> {} & b11 <> {} & b12 <> {} & b13 <> {} & b14 <> {} & b15 <> {} & b16 <> {} & b17 <> {} & b18 <> {} holds
for b19 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:]
for b20 being Element of [:b10,b11,b12,b13,b14,b15,b16,b17,b18:] st b19 = b20 holds
( b19 `1 = b20 `1 & b19 `2 = b20 `2 & b19 `3 = b20 `3 & b19 `4 = b20 `4 & b19 `5 = b20 `5 & b19 `6 = b20 `6 & b19 `7 = b20 `7 & b19 `8 = b20 `8 & b19 `9 = b20 `9 )
proof end;

theorem Th44: :: MCART_6:44
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set
for b10 being Subset of b1
for b11 being Subset of b2
for b12 being Subset of b3
for b13 being Subset of b4
for b14 being Subset of b5
for b15 being Subset of b6
for b16 being Subset of b7
for b17 being Subset of b8
for b18 being Subset of b9
for b19 being Element of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] st b19 in [:b10,b11,b12,b13,b14,b15,b16,b17,b18:] holds
( b19 `1 in b10 & b19 `2 in b11 & b19 `3 in b12 & b19 `4 in b13 & b19 `5 in b14 & b19 `6 in b15 & b19 `7 in b16 & b19 `8 in b17 & b19 `9 in b18 )
proof end;

theorem Th45: :: MCART_6:45
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18 being set st b1 c= b2 & b3 c= b4 & b5 c= b6 & b7 c= b8 & b9 c= b10 & b11 c= b12 & b13 c= b14 & b15 c= b16 & b17 c= b18 holds
[:b1,b3,b5,b7,b9,b11,b13,b15,b17:] c= [:b2,b4,b6,b8,b10,b12,b14,b16,b18:]
proof end;

theorem Th46: :: MCART_6:46
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set
for b10 being Subset of b1
for b11 being Subset of b2
for b12 being Subset of b3
for b13 being Subset of b4
for b14 being Subset of b5
for b15 being Subset of b6
for b16 being Subset of b7
for b17 being Subset of b8
for b18 being Subset of b9 holds [:b10,b11,b12,b13,b14,b15,b16,b17,b18:] is Subset of [:b1,b2,b3,b4,b5,b6,b7,b8,b9:] by Th45;