:: MCART_4 semantic presentation

theorem Th1: :: MCART_4:1

for b₁ being set st b₁ <> {} holds
ex b₂ being set st
( b₂ in b₁ & ( for b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂ being set st b₃ in b₄ & b₄ in b₅ & b₅ in b₆ & b₆ in b₇ & b₇ in b₈ & b₈ in b₉ & b₉ in b₁₀ & b₁₀ in b₁₁ & b₁₁ in b₁₂ & b₁₂ in b₂ holds
b₃ misses b₁ ) )

proof end;

theorem Th2: :: MCART_4:2

for b₁ being set st b₁ <> {} holds
ex b₂ being set st
( b₂ in b₁ & ( for b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃ being set st b₃ in b₄ & b₄ in b₅ & b₅ in b₆ & b₆ in b₇ & b₇ in b₈ & b₈ in b₉ & b₉ in b₁₀ & b₁₀ in b₁₁ & b₁₁ in b₁₂ & b₁₂ in b₁₃ & b₁₃ in b₂ holds
b₃ misses b₁ ) )

proof end;

definition

let c₁, c₂, c₃, c₄, c₅, c₆, c₇ be set ;
func [c₁,c₂,c₃,c₄,c₅,c₆,c₇] -> set equals :: MCART_4:def 1
[[a₁,a₂,a₃,a₄,a₅,a₆],a₇];
correctness ;

end;

:: deftheorem Def1 defines [ MCART_4:def 1 :

theorem Th3: :: MCART_4:3

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds [b₁,b₂,b₃,b₄,b₅,b₆,b₇] = [[[[[[b₁,b₂],b₃],b₄],b₅],b₆],b₇]

proof end;

theorem Th4: :: MCART_4:4

canceled;

theorem Th5: :: MCART_4:5

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds [b₁,b₂,b₃,b₄,b₅,b₆,b₇] = [[b₁,b₂,b₃,b₄,b₅],b₆,b₇]

proof end;

theorem Th6: :: MCART_4:6

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds [b₁,b₂,b₃,b₄,b₅,b₆,b₇] = [[b₁,b₂,b₃,b₄],b₅,b₆,b₇]

proof end;

theorem Th7: :: MCART_4:7

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds [b₁,b₂,b₃,b₄,b₅,b₆,b₇] = [[b₁,b₂,b₃],b₄,b₅,b₆,b₇]

proof end;

theorem Th8: :: MCART_4:8

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds [b₁,b₂,b₃,b₄,b₅,b₆,b₇] = [[b₁,b₂],b₃,b₄,b₅,b₆,b₇]

proof end;

theorem Th9: :: MCART_4:9

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃, b₁₄ being set st [b₁,b₂,b₃,b₄,b₅,b₆,b₇] = [b₈,b₉,b₁₀,b₁₁,b₁₂,b₁₃,b₁₄] holds
( b₁ = b₈ & b₂ = b₉ & b₃ = b₁₀ & b₄ = b₁₁ & b₅ = b₁₂ & b₆ = b₁₃ & b₇ = b₁₄ )

proof end;

theorem Th10: :: MCART_4:10

for b₁ being set st b₁ <> {} holds
ex b₂ being set st
( b₂ in b₁ & ( for b₃, b₄, b₅, b₆, b₇, b₈, b₉ being set holds
( ( not b₃ in b₁ & not b₄ in b₁ ) or not b₂ = [b₃,b₄,b₅,b₆,b₇,b₈,b₉] ) ) )

proof end;

definition

let c₁, c₂, c₃, c₄, c₅, c₆, c₇ be set ;
func [:c₁,c₂,c₃,c₄,c₅,c₆,c₇:] -> set equals :: MCART_4:def 2
[:[:a₁,a₂,a₃,a₄,a₅,a₆:],a₇:];
correctness ;

end;

:: deftheorem Def2 defines [: MCART_4:def 2 :

theorem Th11: :: MCART_4:11

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds [:b₁,b₂,b₃,b₄,b₅,b₆,b₇:] = [:[:[:[:[:[:b₁,b₂:],b₃:],b₄:],b₅:],b₆:],b₇:]

proof end;

theorem Th12: :: MCART_4:12

canceled;

theorem Th13: :: MCART_4:13

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds [:b₁,b₂,b₃,b₄,b₅,b₆,b₇:] = [:[:b₁,b₂,b₃,b₄,b₅:],b₆,b₇:]

proof end;

theorem Th14: :: MCART_4:14

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds [:b₁,b₂,b₃,b₄,b₅,b₆,b₇:] = [:[:b₁,b₂,b₃,b₄:],b₅,b₆,b₇:]

proof end;

theorem Th15: :: MCART_4:15

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds [:b₁,b₂,b₃,b₄,b₅,b₆,b₇:] = [:[:b₁,b₂,b₃:],b₄,b₅,b₆,b₇:]

proof end;

theorem Th16: :: MCART_4:16

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds [:b₁,b₂,b₃,b₄,b₅,b₆,b₇:] = [:[:b₁,b₂:],b₃,b₄,b₅,b₆,b₇:]

proof end;

theorem Th17: :: MCART_4:17

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds
( ( b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & b₇ <> {} ) iff [:b₁,b₂,b₃,b₄,b₅,b₆,b₇:] <> {} )

proof end;

theorem Th18: :: MCART_4:18

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃, b₁₄ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & b₇ <> {} & [:b₁,b₂,b₃,b₄,b₅,b₆,b₇:] = [:b₈,b₉,b₁₀,b₁₁,b₁₂,b₁₃,b₁₄:] holds
( b₁ = b₈ & b₂ = b₉ & b₃ = b₁₀ & b₄ = b₁₁ & b₅ = b₁₂ & b₆ = b₁₃ & b₇ = b₁₄ )

proof end;

theorem Th19: :: MCART_4:19

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃, b₁₄ being set st [:b₁,b₂,b₃,b₄,b₅,b₆,b₇:] <> {} & [:b₁,b₂,b₃,b₄,b₅,b₆,b₇:] = [:b₈,b₉,b₁₀,b₁₁,b₁₂,b₁₃,b₁₄:] holds
( b₁ = b₈ & b₂ = b₉ & b₃ = b₁₀ & b₄ = b₁₁ & b₅ = b₁₂ & b₆ = b₁₃ & b₇ = b₁₄ )

proof end;

theorem Th20: :: MCART_4:20

for b₁, b₂ being set st [:b₁,b₁,b₁,b₁,b₁,b₁,b₁:] = [:b₂,b₂,b₂,b₂,b₂,b₂,b₂:] holds
b₁ = b₂

proof end;

theorem Th21: :: MCART_4:21

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & b₇ <> {} holds
for b₈ being Element of [:b₁,b₂,b₃,b₄,b₅,b₆,b₇:] ex b₉ being Element of b₁ex b₁₀ being Element of b₂ex b₁₁ being Element of b₃ex b₁₂ being Element of b₄ex b₁₃ being Element of b₅ex b₁₄ being Element of b₆ex b₁₅ being Element of b₇ st b₈ = [b₉,b₁₀,b₁₁,b₁₂,b₁₃,b₁₄,b₁₅]

proof end;

definition

let c₁, c₂, c₃, c₄, c₅, c₆, c₇ be set ;
assume E11: ( c₁ <> {} & c₂ <> {} & c₃ <> {} & c₄ <> {} & c₅ <> {} & c₆ <> {} & c₇ <> {} ) ;
let c₈ be Element of [:c₁,c₂,c₃,c₄,c₅,c₆,c₇:];
func c₈ `1 -> Element of a₁ means :Def3: :: MCART_4:def 3
for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set st a₈ = [b₁,b₂,b₃,b₄,b₅,b₆,b₇] holds
a₉ = b₁;
existence

proof end;

proof end;

func c₈ `2 -> Element of a₂ means :Def4: :: MCART_4:def 4
for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set st a₈ = [b₁,b₂,b₃,b₄,b₅,b₆,b₇] holds
a₉ = b₂;
existence

proof end;

proof end;

func c₈ `3 -> Element of a₃ means :Def5: :: MCART_4:def 5
for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set st a₈ = [b₁,b₂,b₃,b₄,b₅,b₆,b₇] holds
a₉ = b₃;
existence

proof end;

proof end;

func c₈ `4 -> Element of a₄ means :Def6: :: MCART_4:def 6
for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set st a₈ = [b₁,b₂,b₃,b₄,b₅,b₆,b₇] holds
a₉ = b₄;
existence

proof end;

proof end;

func c₈ `5 -> Element of a₅ means :Def7: :: MCART_4:def 7
for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set st a₈ = [b₁,b₂,b₃,b₄,b₅,b₆,b₇] holds
a₉ = b₅;
existence

proof end;

proof end;

func c₈ `6 -> Element of a₆ means :Def8: :: MCART_4:def 8
for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set st a₈ = [b₁,b₂,b₃,b₄,b₅,b₆,b₇] holds
a₉ = b₆;
existence

proof end;

proof end;

func c₈ `7 -> Element of a₇ means :Def9: :: MCART_4:def 9
for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set st a₈ = [b₁,b₂,b₃,b₄,b₅,b₆,b₇] holds
a₉ = b₇;
existence

proof end;

proof end;

end;

:: deftheorem Def3 defines `1 MCART_4:def 3 :

:: deftheorem Def4 defines `2 MCART_4:def 4 :

:: deftheorem Def5 defines `3 MCART_4:def 5 :

:: deftheorem Def6 defines `4 MCART_4:def 6 :

:: deftheorem Def7 defines `5 MCART_4:def 7 :

:: deftheorem Def8 defines `6 MCART_4:def 8 :

:: deftheorem Def9 defines `7 MCART_4:def 9 :

theorem Th22: :: MCART_4:22

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & b₇ <> {} holds
for b₈ being Element of [:b₁,b₂,b₃,b₄,b₅,b₆,b₇:]
for b₉, b₁₀, b₁₁, b₁₂, b₁₃, b₁₄, b₁₅ being set st b₈ = [b₉,b₁₀,b₁₁,b₁₂,b₁₃,b₁₄,b₁₅] holds
( b₈ `1 = b₉ & b₈ `2 = b₁₀ & b₈ `3 = b₁₁ & b₈ `4 = b₁₂ & b₈ `5 = b₁₃ & b₈ `6 = b₁₄ & b₈ `7 = b₁₅ ) by Def3, Def4, Def5, Def6, Def7, Def8, Def9;

theorem Th23: :: MCART_4:23

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & b₇ <> {} holds
for b₈ being Element of [:b₁,b₂,b₃,b₄,b₅,b₆,b₇:] holds b₈ = [(b₈ `1 ),(b₈ `2 ),(b₈ `3 ),(b₈ `4 ),(b₈ `5 ),(b₈ `6 ),(b₈ `7 )]

proof end;

theorem Th24: :: MCART_4:24

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & b₇ <> {} holds
for b₈ being Element of [:b₁,b₂,b₃,b₄,b₅,b₆,b₇:] holds
( b₈ `1 = (((((b₈ `1 ) `1 ) `1 ) `1 ) `1 ) `1 & b₈ `2 = (((((b₈ `1 ) `1 ) `1 ) `1 ) `1 ) `2 & b₈ `3 = ((((b₈ `1 ) `1 ) `1 ) `1 ) `2 & b₈ `4 = (((b₈ `1 ) `1 ) `1 ) `2 & b₈ `5 = ((b₈ `1 ) `1 ) `2 & b₈ `6 = (b₈ `1 ) `2 & b₈ `7 = b₈ `2 )

proof end;

theorem Th25: :: MCART_4:25

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set st ( b₁ c= [:b₁,b₂,b₃,b₄,b₅,b₆,b₇:] or b₁ c= [:b₂,b₃,b₄,b₅,b₆,b₇,b₁:] or b₁ c= [:b₃,b₄,b₅,b₆,b₇,b₁,b₂:] or b₁ c= [:b₄,b₅,b₆,b₇,b₁,b₂,b₃:] or b₁ c= [:b₅,b₆,b₇,b₁,b₂,b₃,b₄:] or b₁ c= [:b₆,b₇,b₁,b₂,b₃,b₄,b₅:] or b₁ c= [:b₇,b₁,b₂,b₃,b₄,b₅,b₆:] ) holds
b₁ = {}

proof end;

theorem Th26: :: MCART_4:26

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃, b₁₄ being set st [:b₁,b₂,b₃,b₄,b₅,b₆,b₇:] meets [:b₈,b₉,b₁₀,b₁₁,b₁₂,b₁₃,b₁₄:] holds
( b₁ meets b₈ & b₂ meets b₉ & b₃ meets b₁₀ & b₄ meets b₁₁ & b₅ meets b₁₂ & b₆ meets b₁₃ & b₇ meets b₁₄ )

proof end;

theorem Th27: :: MCART_4:27

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds [:{b₁},{b₂},{b₃},{b₄},{b₅},{b₆},{b₇}:] = {[b₁,b₂,b₃,b₄,b₅,b₆,b₇]}

proof end;

theorem Th28: :: MCART_4:28

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set
for b₈ being Element of [:b₁,b₂,b₃,b₄,b₅,b₆,b₇:] st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & b₇ <> {} holds
for b₉, b₁₀, b₁₁, b₁₂, b₁₃, b₁₄, b₁₅ being set st b₈ = [b₉,b₁₀,b₁₁,b₁₂,b₁₃,b₁₄,b₁₅] holds
( b₈ `1 = b₉ & b₈ `2 = b₁₀ & b₈ `3 = b₁₁ & b₈ `4 = b₁₂ & b₈ `5 = b₁₃ & b₈ `6 = b₁₄ & b₈ `7 = b₁₅ ) by Def3, Def4, Def5, Def6, Def7, Def8, Def9;

theorem Th29: :: MCART_4:29

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set
for b₉ being Element of [:b₂,b₃,b₄,b₅,b₆,b₇,b₈:] st b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & b₇ <> {} & b₈ <> {} & ( for b₁₀ being Element of b₂
for b₁₁ being Element of b₃
for b₁₂ being Element of b₄
for b₁₃ being Element of b₅
for b₁₄ being Element of b₆
for b₁₅ being Element of b₇
for b₁₆ being Element of b₈ st b₉ = [b₁₀,b₁₁,b₁₂,b₁₃,b₁₄,b₁₅,b₁₆] holds
b₁ = b₁₀ ) holds
b₁ = b₉ `1

proof end;

theorem Th30: :: MCART_4:30

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set
for b₉ being Element of [:b₂,b₃,b₄,b₅,b₆,b₇,b₈:] st b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & b₇ <> {} & b₈ <> {} & ( for b₁₀ being Element of b₂
for b₁₁ being Element of b₃
for b₁₂ being Element of b₄
for b₁₃ being Element of b₅
for b₁₄ being Element of b₆
for b₁₅ being Element of b₇
for b₁₆ being Element of b₈ st b₉ = [b₁₀,b₁₁,b₁₂,b₁₃,b₁₄,b₁₅,b₁₆] holds
b₁ = b₁₁ ) holds
b₁ = b₉ `2

proof end;

theorem Th31: :: MCART_4:31

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set
for b₉ being Element of [:b₂,b₃,b₄,b₅,b₆,b₇,b₈:] st b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & b₇ <> {} & b₈ <> {} & ( for b₁₀ being Element of b₂
for b₁₁ being Element of b₃
for b₁₂ being Element of b₄
for b₁₃ being Element of b₅
for b₁₄ being Element of b₆
for b₁₅ being Element of b₇
for b₁₆ being Element of b₈ st b₉ = [b₁₀,b₁₁,b₁₂,b₁₃,b₁₄,b₁₅,b₁₆] holds
b₁ = b₁₂ ) holds
b₁ = b₉ `3

proof end;

theorem Th32: :: MCART_4:32

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set
for b₉ being Element of [:b₂,b₃,b₄,b₅,b₆,b₇,b₈:] st b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & b₇ <> {} & b₈ <> {} & ( for b₁₀ being Element of b₂
for b₁₁ being Element of b₃
for b₁₂ being Element of b₄
for b₁₃ being Element of b₅
for b₁₄ being Element of b₆
for b₁₅ being Element of b₇
for b₁₆ being Element of b₈ st b₉ = [b₁₀,b₁₁,b₁₂,b₁₃,b₁₄,b₁₅,b₁₆] holds
b₁ = b₁₃ ) holds
b₁ = b₉ `4

proof end;

theorem Th33: :: MCART_4:33

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set
for b₉ being Element of [:b₂,b₃,b₄,b₅,b₆,b₇,b₈:] st b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & b₇ <> {} & b₈ <> {} & ( for b₁₀ being Element of b₂
for b₁₁ being Element of b₃
for b₁₂ being Element of b₄
for b₁₃ being Element of b₅
for b₁₄ being Element of b₆
for b₁₅ being Element of b₇
for b₁₆ being Element of b₈ st b₉ = [b₁₀,b₁₁,b₁₂,b₁₃,b₁₄,b₁₅,b₁₆] holds
b₁ = b₁₄ ) holds
b₁ = b₉ `5

proof end;

theorem Th34: :: MCART_4:34

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set
for b₉ being Element of [:b₂,b₃,b₄,b₅,b₆,b₇,b₈:] st b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & b₇ <> {} & b₈ <> {} & ( for b₁₀ being Element of b₂
for b₁₁ being Element of b₃
for b₁₂ being Element of b₄
for b₁₃ being Element of b₅
for b₁₄ being Element of b₆
for b₁₅ being Element of b₇
for b₁₆ being Element of b₈ st b₉ = [b₁₀,b₁₁,b₁₂,b₁₃,b₁₄,b₁₅,b₁₆] holds
b₁ = b₁₅ ) holds
b₁ = b₉ `6

proof end;

theorem Th35: :: MCART_4:35

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set
for b₉ being Element of [:b₂,b₃,b₄,b₅,b₆,b₇,b₈:] st b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & b₇ <> {} & b₈ <> {} & ( for b₁₀ being Element of b₂
for b₁₁ being Element of b₃
for b₁₂ being Element of b₄
for b₁₃ being Element of b₅
for b₁₄ being Element of b₆
for b₁₅ being Element of b₇
for b₁₆ being Element of b₈ st b₉ = [b₁₀,b₁₁,b₁₂,b₁₃,b₁₄,b₁₅,b₁₆] holds
b₁ = b₁₆ ) holds
b₁ = b₉ `7

proof end;

theorem Th36: :: MCART_4:36

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set st b₁ in [:b₂,b₃,b₄,b₅,b₆,b₇,b₈:] holds
ex b₉, b₁₀, b₁₁, b₁₂, b₁₃, b₁₄, b₁₅ being set st
( b₉ in b₂ & b₁₀ in b₃ & b₁₁ in b₄ & b₁₂ in b₅ & b₁₃ in b₆ & b₁₄ in b₇ & b₁₅ in b₈ & b₁ = [b₉,b₁₀,b₁₁,b₁₂,b₁₃,b₁₄,b₁₅] )

proof end;

theorem Th37: :: MCART_4:37

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃, b₁₄ being set holds
( [b₁,b₂,b₃,b₄,b₅,b₆,b₇] in [:b₈,b₉,b₁₀,b₁₁,b₁₂,b₁₃,b₁₄:] iff ( b₁ in b₈ & b₂ in b₉ & b₃ in b₁₀ & b₄ in b₁₁ & b₅ in b₁₂ & b₆ in b₁₃ & b₇ in b₁₄ ) )

proof end;

theorem Th38: :: MCART_4:38

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set st ( for b₉ being set holds
( b₉ in b₈ iff ex b₁₀, b₁₁, b₁₂, b₁₃, b₁₄, b₁₅, b₁₆ being set st
( b₁₀ in b₁ & b₁₁ in b₂ & b₁₂ in b₃ & b₁₃ in b₄ & b₁₄ in b₅ & b₁₅ in b₆ & b₁₆ in b₇ & b₉ = [b₁₀,b₁₁,b₁₂,b₁₃,b₁₄,b₁₅,b₁₆] ) ) ) holds
b₈ = [:b₁,b₂,b₃,b₄,b₅,b₆,b₇:]

proof end;

theorem Th39: :: MCART_4:39

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃, b₁₄ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & b₇ <> {} & b₈ <> {} & b₉ <> {} & b₁₀ <> {} & b₁₁ <> {} & b₁₂ <> {} & b₁₃ <> {} & b₁₄ <> {} holds
for b₁₅ being Element of [:b₁,b₂,b₃,b₄,b₅,b₆,b₇:]
for b₁₆ being Element of [:b₈,b₉,b₁₀,b₁₁,b₁₂,b₁₃,b₁₄:] st b₁₅ = b₁₆ holds
( b₁₅ `1 = b₁₆ `1 & b₁₅ `2 = b₁₆ `2 & b₁₅ `3 = b₁₆ `3 & b₁₅ `4 = b₁₆ `4 & b₁₅ `5 = b₁₆ `5 & b₁₅ `6 = b₁₆ `6 & b₁₅ `7 = b₁₆ `7 )

proof end;

theorem Th40: :: MCART_4:40

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set
for b₈ being Subset of b₁
for b₉ being Subset of b₂
for b₁₀ being Subset of b₃
for b₁₁ being Subset of b₄
for b₁₂ being Subset of b₅
for b₁₃ being Subset of b₆
for b₁₄ being Subset of b₇
for b₁₅ being Element of [:b₁,b₂,b₃,b₄,b₅,b₆,b₇:] st b₁₅ in [:b₈,b₉,b₁₀,b₁₁,b₁₂,b₁₃,b₁₄:] holds
( b₁₅ `1 in b₈ & b₁₅ `2 in b₉ & b₁₅ `3 in b₁₀ & b₁₅ `4 in b₁₁ & b₁₅ `5 in b₁₂ & b₁₅ `6 in b₁₃ & b₁₅ `7 in b₁₄ )

proof end;

theorem Th41: :: MCART_4:41

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃, b₁₄ being set st b₁ c= b₈ & b₂ c= b₉ & b₃ c= b₁₀ & b₄ c= b₁₁ & b₅ c= b₁₂ & b₆ c= b₁₃ & b₇ c= b₁₄ holds
[:b₁,b₂,b₃,b₄,b₅,b₆,b₇:] c= [:b₈,b₉,b₁₀,b₁₁,b₁₂,b₁₃,b₁₄:]

proof end;

theorem Th42: :: MCART_4:42

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set
for b₈ being Subset of b₁
for b₉ being Subset of b₂
for b₁₀ being Subset of b₃
for b₁₁ being Subset of b₄
for b₁₂ being Subset of b₅
for b₁₃ being Subset of b₆
for b₁₄ being Subset of b₇ holds [:b₈,b₉,b₁₀,b₁₁,b₁₂,b₁₃,b₁₄:] is Subset of [:b₁,b₂,b₃,b₄,b₅,b₆,b₇:] by Th41;