:: SETLIM_2 semantic presentation

theorem Th1: :: SETLIM_2:1

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ holds (inferior_setsequence b₃) . b₁ = Intersection (b₃ ^\ b₁)

proof end;

theorem Th2: :: SETLIM_2:2

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ holds (superior_setsequence b₃) . b₁ = Union (b₃ ^\ b₁)

proof end;

definition

let c₁ be set ;
let c₂, c₃ be SetSequence of c₁;
func c₂ (/\) c₃ -> SetSequence of a₁ means :Def1: :: SETLIM_2:def 1
for b₁ being Nat holds a₄ . b₁ = (a₂ . b₁) /\ (a₃ . b₁);
existence

proof end;

proof end;

commutativity ;
func c₂ (\/) c₃ -> SetSequence of a₁ means :Def2: :: SETLIM_2:def 2
for b₁ being Nat holds a₄ . b₁ = (a₂ . b₁) \/ (a₃ . b₁);
existence

proof end;

proof end;

commutativity ;
func c₂ (\) c₃ -> SetSequence of a₁ means :Def3: :: SETLIM_2:def 3
for b₁ being Nat holds a₄ . b₁ = (a₂ . b₁) \ (a₃ . b₁);
existence

proof end;

proof end;

func c₂ (\+\) c₃ -> SetSequence of a₁ means :Def4: :: SETLIM_2:def 4
for b₁ being Nat holds a₄ . b₁ = (a₂ . b₁) \+\ (a₃ . b₁);
existence

proof end;

proof end;

commutativity ;

end;

:: deftheorem Def1 defines (/\) SETLIM_2:def 1 :

:: deftheorem Def2 defines (\/) SETLIM_2:def 2 :

:: deftheorem Def3 defines (\) SETLIM_2:def 3 :

:: deftheorem Def4 defines (\+\) SETLIM_2:def 4 :

theorem Th3: :: SETLIM_2:3

for b₁ being set
for b₂, b₃ being SetSequence of b₁ holds b₂ (\+\) b₃ = (b₂ (\) b₃) (\/) (b₃ (\) b₂)

proof end;

theorem Th4: :: SETLIM_2:4

for b₁ being Nat
for b₂ being set
for b₃, b₄ being SetSequence of b₂ holds (b₃ (/\) b₄) ^\ b₁ = (b₃ ^\ b₁) (/\) (b₄ ^\ b₁)

proof end;

theorem Th5: :: SETLIM_2:5

for b₁ being Nat
for b₂ being set
for b₃, b₄ being SetSequence of b₂ holds (b₃ (\/) b₄) ^\ b₁ = (b₃ ^\ b₁) (\/) (b₄ ^\ b₁)

proof end;

theorem Th6: :: SETLIM_2:6

for b₁ being Nat
for b₂ being set
for b₃, b₄ being SetSequence of b₂ holds (b₃ (\) b₄) ^\ b₁ = (b₃ ^\ b₁) (\) (b₄ ^\ b₁)

proof end;

theorem Th7: :: SETLIM_2:7

for b₁ being Nat
for b₂ being set
for b₃, b₄ being SetSequence of b₂ holds (b₃ (\+\) b₄) ^\ b₁ = (b₃ ^\ b₁) (\+\) (b₄ ^\ b₁)

proof end;

theorem Th8: :: SETLIM_2:8

for b₁ being set
for b₂, b₃ being SetSequence of b₁ holds Union (b₂ (/\) b₃) c= (Union b₂) /\ (Union b₃)

proof end;

theorem Th9: :: SETLIM_2:9

for b₁ being set
for b₂, b₃ being SetSequence of b₁ holds Union (b₂ (\/) b₃) = (Union b₂) \/ (Union b₃)

proof end;

theorem Th10: :: SETLIM_2:10

for b₁ being set
for b₂, b₃ being SetSequence of b₁ holds (Union b₂) \ (Union b₃) c= Union (b₂ (\) b₃)

proof end;

theorem Th11: :: SETLIM_2:11

for b₁ being set
for b₂, b₃ being SetSequence of b₁ holds (Union b₂) \+\ (Union b₃) c= Union (b₂ (\+\) b₃)

proof end;

theorem Th12: :: SETLIM_2:12

for b₁ being set
for b₂, b₃ being SetSequence of b₁ holds Intersection (b₂ (/\) b₃) = (Intersection b₂) /\ (Intersection b₃)

proof end;

theorem Th13: :: SETLIM_2:13

for b₁ being set
for b₂, b₃ being SetSequence of b₁ holds (Intersection b₂) \/ (Intersection b₃) c= Intersection (b₂ (\/) b₃)

proof end;

theorem Th14: :: SETLIM_2:14

for b₁ being set
for b₂, b₃ being SetSequence of b₁ holds Intersection (b₂ (\) b₃) c= (Intersection b₂) \ (Intersection b₃)

proof end;

definition

let c₁ be set ;
let c₂ be SetSequence of c₁;
let c₃ be Subset of c₁;
func c₃ (/\) c₂ -> SetSequence of a₁ means :Def5: :: SETLIM_2:def 5
for b₁ being Nat holds a₄ . b₁ = a₃ /\ (a₂ . b₁);
existence

proof end;

proof end;

func c₃ (\/) c₂ -> SetSequence of a₁ means :Def6: :: SETLIM_2:def 6
for b₁ being Nat holds a₄ . b₁ = a₃ \/ (a₂ . b₁);
existence

proof end;

proof end;

func c₃ (\) c₂ -> SetSequence of a₁ means :Def7: :: SETLIM_2:def 7
for b₁ being Nat holds a₄ . b₁ = a₃ \ (a₂ . b₁);
existence

proof end;

proof end;

func c₂ (\) c₃ -> SetSequence of a₁ means :Def8: :: SETLIM_2:def 8
for b₁ being Nat holds a₄ . b₁ = (a₂ . b₁) \ a₃;
existence

proof end;

proof end;

func c₃ (\+\) c₂ -> SetSequence of a₁ means :Def9: :: SETLIM_2:def 9
for b₁ being Nat holds a₄ . b₁ = a₃ \+\ (a₂ . b₁);
existence

proof end;

proof end;

end;

:: deftheorem Def5 defines (/\) SETLIM_2:def 5 :

:: deftheorem Def6 defines (\/) SETLIM_2:def 6 :

:: deftheorem Def7 defines (\) SETLIM_2:def 7 :

:: deftheorem Def8 defines (\) SETLIM_2:def 8 :

:: deftheorem Def9 defines (\+\) SETLIM_2:def 9 :

theorem Th15: :: SETLIM_2:15

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds b₂ (\+\) b₃ = (b₂ (\) b₃) (\/) (b₃ (\) b₂)

proof end;

theorem Th16: :: SETLIM_2:16

for b₁ being Nat
for b₂ being set
for b₃ being Subset of b₂
for b₄ being SetSequence of b₂ holds (b₃ (/\) b₄) ^\ b₁ = b₃ (/\) (b₄ ^\ b₁)

proof end;

theorem Th17: :: SETLIM_2:17

for b₁ being Nat
for b₂ being set
for b₃ being Subset of b₂
for b₄ being SetSequence of b₂ holds (b₃ (\/) b₄) ^\ b₁ = b₃ (\/) (b₄ ^\ b₁)

proof end;

theorem Th18: :: SETLIM_2:18

for b₁ being Nat
for b₂ being set
for b₃ being Subset of b₂
for b₄ being SetSequence of b₂ holds (b₃ (\) b₄) ^\ b₁ = b₃ (\) (b₄ ^\ b₁)

proof end;

theorem Th19: :: SETLIM_2:19

for b₁ being Nat
for b₂ being set
for b₃ being Subset of b₂
for b₄ being SetSequence of b₂ holds (b₄ (\) b₃) ^\ b₁ = (b₄ ^\ b₁) (\) b₃

proof end;

theorem Th20: :: SETLIM_2:20

for b₁ being Nat
for b₂ being set
for b₃ being Subset of b₂
for b₄ being SetSequence of b₂ holds (b₃ (\+\) b₄) ^\ b₁ = b₃ (\+\) (b₄ ^\ b₁)

proof end;

theorem Th21: :: SETLIM_2:21

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is non-increasing holds
b₂ (/\) b₃ is non-increasing

proof end;

theorem Th22: :: SETLIM_2:22

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is non-decreasing holds
b₂ (/\) b₃ is non-decreasing

proof end;

theorem Th23: :: SETLIM_2:23

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is monotone holds
b₂ (/\) b₃ is monotone

proof end;

theorem Th24: :: SETLIM_2:24

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is non-increasing holds
b₂ (\/) b₃ is non-increasing

proof end;

theorem Th25: :: SETLIM_2:25

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is non-decreasing holds
b₂ (\/) b₃ is non-decreasing

proof end;

theorem Th26: :: SETLIM_2:26

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is monotone holds
b₂ (\/) b₃ is monotone

proof end;

theorem Th27: :: SETLIM_2:27

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is non-increasing holds
b₂ (\) b₃ is non-decreasing

proof end;

theorem Th28: :: SETLIM_2:28

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is non-decreasing holds
b₂ (\) b₃ is non-increasing

proof end;

theorem Th29: :: SETLIM_2:29

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is monotone holds
b₂ (\) b₃ is monotone

proof end;

theorem Th30: :: SETLIM_2:30

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is non-increasing holds
b₃ (\) b₂ is non-increasing

proof end;

theorem Th31: :: SETLIM_2:31

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is non-decreasing holds
b₃ (\) b₂ is non-decreasing

proof end;

theorem Th32: :: SETLIM_2:32

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is monotone holds
b₃ (\) b₂ is monotone

proof end;

theorem Th33: :: SETLIM_2:33

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds Intersection (b₂ (/\) b₃) = b₂ /\ (Intersection b₃)

proof end;

theorem Th34: :: SETLIM_2:34

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds Intersection (b₂ (\/) b₃) = b₂ \/ (Intersection b₃)

proof end;

theorem Th35: :: SETLIM_2:35

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds Intersection (b₂ (\) b₃) c= b₂ \ (Intersection b₃)

proof end;

theorem Th36: :: SETLIM_2:36

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds Intersection (b₃ (\) b₂) = (Intersection b₃) \ b₂

proof end;

theorem Th37: :: SETLIM_2:37

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds Intersection (b₂ (\+\) b₃) c= b₂ \+\ (Intersection b₃)

proof end;

theorem Th38: :: SETLIM_2:38

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds Union (b₂ (/\) b₃) = b₂ /\ (Union b₃)

proof end;

theorem Th39: :: SETLIM_2:39

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds Union (b₂ (\/) b₃) = b₂ \/ (Union b₃)

proof end;

theorem Th40: :: SETLIM_2:40

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds b₂ \ (Union b₃) c= Union (b₂ (\) b₃)

proof end;

theorem Th41: :: SETLIM_2:41

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds Union (b₃ (\) b₂) = (Union b₃) \ b₂

proof end;

theorem Th42: :: SETLIM_2:42

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds b₂ \+\ (Union b₃) c= Union (b₂ (\+\) b₃)

proof end;

theorem Th43: :: SETLIM_2:43

for b₁ being Nat
for b₂ being set
for b₃, b₄ being SetSequence of b₂ holds (inferior_setsequence (b₃ (/\) b₄)) . b₁ = ((inferior_setsequence b₃) . b₁) /\ ((inferior_setsequence b₄) . b₁)

proof end;

theorem Th44: :: SETLIM_2:44

for b₁ being Nat
for b₂ being set
for b₃, b₄ being SetSequence of b₂ holds ((inferior_setsequence b₃) . b₁) \/ ((inferior_setsequence b₄) . b₁) c= (inferior_setsequence (b₃ (\/) b₄)) . b₁

proof end;

theorem Th45: :: SETLIM_2:45

for b₁ being Nat
for b₂ being set
for b₃, b₄ being SetSequence of b₂ holds (inferior_setsequence (b₃ (\) b₄)) . b₁ c= ((inferior_setsequence b₃) . b₁) \ ((inferior_setsequence b₄) . b₁)

proof end;

theorem Th46: :: SETLIM_2:46

for b₁ being Nat
for b₂ being set
for b₃, b₄ being SetSequence of b₂ holds (superior_setsequence (b₃ (/\) b₄)) . b₁ c= ((superior_setsequence b₃) . b₁) /\ ((superior_setsequence b₄) . b₁)

proof end;

theorem Th47: :: SETLIM_2:47

for b₁ being Nat
for b₂ being set
for b₃, b₄ being SetSequence of b₂ holds (superior_setsequence (b₃ (\/) b₄)) . b₁ = ((superior_setsequence b₃) . b₁) \/ ((superior_setsequence b₄) . b₁)

proof end;

theorem Th48: :: SETLIM_2:48

for b₁ being Nat
for b₂ being set
for b₃, b₄ being SetSequence of b₂ holds ((superior_setsequence b₃) . b₁) \ ((superior_setsequence b₄) . b₁) c= (superior_setsequence (b₃ (\) b₄)) . b₁

proof end;

theorem Th49: :: SETLIM_2:49

for b₁ being Nat
for b₂ being set
for b₃, b₄ being SetSequence of b₂ holds ((superior_setsequence b₃) . b₁) \+\ ((superior_setsequence b₄) . b₁) c= (superior_setsequence (b₃ (\+\) b₄)) . b₁

proof end;

theorem Th50: :: SETLIM_2:50

for b₁ being Nat
for b₂ being set
for b₃ being Subset of b₂
for b₄ being SetSequence of b₂ holds (inferior_setsequence (b₃ (/\) b₄)) . b₁ = b₃ /\ ((inferior_setsequence b₄) . b₁)

proof end;

theorem Th51: :: SETLIM_2:51

for b₁ being Nat
for b₂ being set
for b₃ being Subset of b₂
for b₄ being SetSequence of b₂ holds (inferior_setsequence (b₃ (\/) b₄)) . b₁ = b₃ \/ ((inferior_setsequence b₄) . b₁)

proof end;

theorem Th52: :: SETLIM_2:52

for b₁ being Nat
for b₂ being set
for b₃ being Subset of b₂
for b₄ being SetSequence of b₂ holds (inferior_setsequence (b₃ (\) b₄)) . b₁ c= b₃ \ ((inferior_setsequence b₄) . b₁)

proof end;

theorem Th53: :: SETLIM_2:53

for b₁ being Nat
for b₂ being set
for b₃ being Subset of b₂
for b₄ being SetSequence of b₂ holds (inferior_setsequence (b₄ (\) b₃)) . b₁ = ((inferior_setsequence b₄) . b₁) \ b₃

proof end;

theorem Th54: :: SETLIM_2:54

for b₁ being Nat
for b₂ being set
for b₃ being Subset of b₂
for b₄ being SetSequence of b₂ holds (inferior_setsequence (b₃ (\+\) b₄)) . b₁ c= b₃ \+\ ((inferior_setsequence b₄) . b₁)

proof end;

theorem Th55: :: SETLIM_2:55

for b₁ being Nat
for b₂ being set
for b₃ being Subset of b₂
for b₄ being SetSequence of b₂ holds (superior_setsequence (b₃ (/\) b₄)) . b₁ = b₃ /\ ((superior_setsequence b₄) . b₁)

proof end;

theorem Th56: :: SETLIM_2:56

for b₁ being Nat
for b₂ being set
for b₃ being Subset of b₂
for b₄ being SetSequence of b₂ holds (superior_setsequence (b₃ (\/) b₄)) . b₁ = b₃ \/ ((superior_setsequence b₄) . b₁)

proof end;

theorem Th57: :: SETLIM_2:57

for b₁ being Nat
for b₂ being set
for b₃ being Subset of b₂
for b₄ being SetSequence of b₂ holds b₃ \ ((superior_setsequence b₄) . b₁) c= (superior_setsequence (b₃ (\) b₄)) . b₁

proof end;

theorem Th58: :: SETLIM_2:58

for b₁ being Nat
for b₂ being set
for b₃ being Subset of b₂
for b₄ being SetSequence of b₂ holds (superior_setsequence (b₄ (\) b₃)) . b₁ = ((superior_setsequence b₄) . b₁) \ b₃

proof end;

theorem Th59: :: SETLIM_2:59

for b₁ being Nat
for b₂ being set
for b₃ being Subset of b₂
for b₄ being SetSequence of b₂ holds b₃ \+\ ((superior_setsequence b₄) . b₁) c= (superior_setsequence (b₃ (\+\) b₄)) . b₁

proof end;

theorem Th60: :: SETLIM_2:60

for b₁ being set
for b₂, b₃ being SetSequence of b₁ holds lim_inf (b₂ (/\) b₃) = (lim_inf b₂) /\ (lim_inf b₃)

proof end;

theorem Th61: :: SETLIM_2:61

for b₁ being set
for b₂, b₃ being SetSequence of b₁ holds (lim_inf b₂) \/ (lim_inf b₃) c= lim_inf (b₂ (\/) b₃)

proof end;

theorem Th62: :: SETLIM_2:62

for b₁ being set
for b₂, b₃ being SetSequence of b₁ holds lim_inf (b₂ (\) b₃) c= (lim_inf b₂) \ (lim_inf b₃)

proof end;

theorem Th63: :: SETLIM_2:63

for b₁ being set
for b₂, b₃ being SetSequence of b₁ st ( b₂ is convergent or b₃ is convergent ) holds
lim_inf (b₂ (\/) b₃) = (lim_inf b₂) \/ (lim_inf b₃)

proof end;

theorem Th64: :: SETLIM_2:64

for b₁ being set
for b₂, b₃ being SetSequence of b₁ st b₂ is convergent holds
lim_inf (b₃ (\) b₂) = (lim_inf b₃) \ (lim_inf b₂)

proof end;

theorem Th65: :: SETLIM_2:65

for b₁ being set
for b₂, b₃ being SetSequence of b₁ st ( b₂ is convergent or b₃ is convergent ) holds
lim_inf (b₂ (\+\) b₃) c= (lim_inf b₂) \+\ (lim_inf b₃)

proof end;

theorem Th66: :: SETLIM_2:66

for b₁ being set
for b₂, b₃ being SetSequence of b₁ st b₂ is convergent & b₃ is convergent holds
lim_inf (b₂ (\+\) b₃) = (lim_inf b₂) \+\ (lim_inf b₃)

proof end;

theorem Th67: :: SETLIM_2:67

for b₁ being set
for b₂, b₃ being SetSequence of b₁ holds lim_sup (b₂ (/\) b₃) c= (lim_sup b₂) /\ (lim_sup b₃)

proof end;

theorem Th68: :: SETLIM_2:68

for b₁ being set
for b₂, b₃ being SetSequence of b₁ holds lim_sup (b₂ (\/) b₃) = (lim_sup b₂) \/ (lim_sup b₃)

proof end;

theorem Th69: :: SETLIM_2:69

for b₁ being set
for b₂, b₃ being SetSequence of b₁ holds (lim_sup b₂) \ (lim_sup b₃) c= lim_sup (b₂ (\) b₃)

proof end;

theorem Th70: :: SETLIM_2:70

for b₁ being set
for b₂, b₃ being SetSequence of b₁ holds (lim_sup b₂) \+\ (lim_sup b₃) c= lim_sup (b₂ (\+\) b₃)

proof end;

theorem Th71: :: SETLIM_2:71

for b₁ being set
for b₂, b₃ being SetSequence of b₁ st ( b₂ is convergent or b₃ is convergent ) holds
lim_sup (b₂ (/\) b₃) = (lim_sup b₂) /\ (lim_sup b₃)

proof end;

theorem Th72: :: SETLIM_2:72

for b₁ being set
for b₂, b₃ being SetSequence of b₁ st b₂ is convergent holds
lim_sup (b₃ (\) b₂) = (lim_sup b₃) \ (lim_sup b₂)

proof end;

theorem Th73: :: SETLIM_2:73

for b₁ being set
for b₂, b₃ being SetSequence of b₁ st b₂ is convergent & b₃ is convergent holds
lim_sup (b₂ (\+\) b₃) = (lim_sup b₂) \+\ (lim_sup b₃)

proof end;

theorem Th74: :: SETLIM_2:74

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds lim_inf (b₂ (/\) b₃) = b₂ /\ (lim_inf b₃)

proof end;

theorem Th75: :: SETLIM_2:75

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds lim_inf (b₂ (\/) b₃) = b₂ \/ (lim_inf b₃)

proof end;

theorem Th76: :: SETLIM_2:76

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds lim_inf (b₂ (\) b₃) c= b₂ \ (lim_inf b₃)

proof end;

theorem Th77: :: SETLIM_2:77

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds lim_inf (b₃ (\) b₂) = (lim_inf b₃) \ b₂

proof end;

theorem Th78: :: SETLIM_2:78

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds lim_inf (b₂ (\+\) b₃) c= b₂ \+\ (lim_inf b₃)

proof end;

theorem Th79: :: SETLIM_2:79

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is convergent holds
lim_inf (b₂ (\) b₃) = b₂ \ (lim_inf b₃)

proof end;

theorem Th80: :: SETLIM_2:80

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is convergent holds
lim_inf (b₂ (\+\) b₃) = b₂ \+\ (lim_inf b₃)

proof end;

theorem Th81: :: SETLIM_2:81

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds lim_sup (b₂ (/\) b₃) = b₂ /\ (lim_sup b₃)

proof end;

theorem Th82: :: SETLIM_2:82

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds lim_sup (b₂ (\/) b₃) = b₂ \/ (lim_sup b₃)

proof end;

theorem Th83: :: SETLIM_2:83

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds b₂ \ (lim_sup b₃) c= lim_sup (b₂ (\) b₃)

proof end;

theorem Th84: :: SETLIM_2:84

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds lim_sup (b₃ (\) b₂) = (lim_sup b₃) \ b₂

proof end;

theorem Th85: :: SETLIM_2:85

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ holds b₂ \+\ (lim_sup b₃) c= lim_sup (b₂ (\+\) b₃)

proof end;

theorem Th86: :: SETLIM_2:86

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is convergent holds
lim_sup (b₂ (\) b₃) = b₂ \ (lim_sup b₃)

proof end;

theorem Th87: :: SETLIM_2:87

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is convergent holds
lim_sup (b₂ (\+\) b₃) = b₂ \+\ (lim_sup b₃)

proof end;

theorem Th88: :: SETLIM_2:88

for b₁ being set
for b₂, b₃ being SetSequence of b₁ st b₂ is convergent & b₃ is convergent holds
( b₂ (/\) b₃ is convergent & lim (b₂ (/\) b₃) = (lim b₂) /\ (lim b₃) )

proof end;

theorem Th89: :: SETLIM_2:89

for b₁ being set
for b₂, b₃ being SetSequence of b₁ st b₂ is convergent & b₃ is convergent holds
( b₂ (\/) b₃ is convergent & lim (b₂ (\/) b₃) = (lim b₂) \/ (lim b₃) )

proof end;

theorem Th90: :: SETLIM_2:90

for b₁ being set
for b₂, b₃ being SetSequence of b₁ st b₂ is convergent & b₃ is convergent holds
( b₂ (\) b₃ is convergent & lim (b₂ (\) b₃) = (lim b₂) \ (lim b₃) )

proof end;

theorem Th91: :: SETLIM_2:91

for b₁ being set
for b₂, b₃ being SetSequence of b₁ st b₂ is convergent & b₃ is convergent holds
( b₂ (\+\) b₃ is convergent & lim (b₂ (\+\) b₃) = (lim b₂) \+\ (lim b₃) )

proof end;

theorem Th92: :: SETLIM_2:92

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is convergent holds
( b₂ (/\) b₃ is convergent & lim (b₂ (/\) b₃) = b₂ /\ (lim b₃) )

proof end;

theorem Th93: :: SETLIM_2:93

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is convergent holds
( b₂ (\/) b₃ is convergent & lim (b₂ (\/) b₃) = b₂ \/ (lim b₃) )

proof end;

theorem Th94: :: SETLIM_2:94

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is convergent holds
( b₂ (\) b₃ is convergent & lim (b₂ (\) b₃) = b₂ \ (lim b₃) )

proof end;

theorem Th95: :: SETLIM_2:95

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is convergent holds
( b₃ (\) b₂ is convergent & lim (b₃ (\) b₂) = (lim b₃) \ b₂ )

proof end;

theorem Th96: :: SETLIM_2:96

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is convergent holds
( b₂ (\+\) b₃ is convergent & lim (b₂ (\+\) b₃) = b₂ \+\ (lim b₃) )

proof end;