:: RCOMP_2 semantic presentation

theorem Th1: :: RCOMP_2:1

canceled;

theorem Th2: :: RCOMP_2:2

for b₁, b₂, b₃ being real number holds
( ( b₁ < b₂ & b₃ < b₂ ) iff max b₁,b₃ < b₂ )

proof end;

definition

let c₁, c₂ be real number ;
func [.c₁,c₂.[ -> Subset of REAL equals :: RCOMP_2:def 1
{ b₁ where B is Real : ( a₁ <= b₁ & b₁ < a₂ ) } ;
coherence

proof end;

func ].c₁,c₂.] -> Subset of REAL equals :: RCOMP_2:def 2
{ b₁ where B is Real : ( a₁ < b₁ & b₁ <= a₂ ) } ;
coherence

proof end;

end;

:: deftheorem Def1 defines [. RCOMP_2:def 1 :

:: deftheorem Def2 defines ]. RCOMP_2:def 2 :

theorem Th3: :: RCOMP_2:3

for b₁, b₂, b₃ being real number holds
( b₁ in [.b₂,b₃.[ iff ( b₂ <= b₁ & b₁ < b₃ ) )

proof end;

theorem Th4: :: RCOMP_2:4

for b₁, b₂, b₃ being real number holds
( b₁ in ].b₂,b₃.] iff ( b₂ < b₁ & b₁ <= b₃ ) )

proof end;

theorem Th5: :: RCOMP_2:5

for b₁, b₂ being real number st b₁ < b₂ holds
[.b₁,b₂.[ = ].b₁,b₂.[ \/ {b₁}

proof end;

theorem Th6: :: RCOMP_2:6

for b₁, b₂ being real number st b₁ < b₂ holds
].b₁,b₂.] = ].b₁,b₂.[ \/ {b₂}

proof end;

theorem Th7: :: RCOMP_2:7

for b₁ being real number holds [.b₁,b₁.[ = {}

proof end;

theorem Th8: :: RCOMP_2:8

for b₁ being real number holds ].b₁,b₁.] = {}

proof end;

theorem Th9: :: RCOMP_2:9

for b₁, b₂ being real number st b₁ <= b₂ holds
[.b₂,b₁.[ = {}

proof end;

theorem Th10: :: RCOMP_2:10

for b₁, b₂ being real number st b₁ <= b₂ holds
].b₂,b₁.] = {}

proof end;

theorem Th11: :: RCOMP_2:11

for b₁, b₂, b₃ being real number st b₁ <= b₂ & b₂ <= b₃ holds
[.b₁,b₂.[ \/ [.b₂,b₃.[ = [.b₁,b₃.[

proof end;

theorem Th12: :: RCOMP_2:12

for b₁, b₂, b₃ being real number st b₁ <= b₂ & b₂ <= b₃ holds
].b₁,b₂.] \/ ].b₂,b₃.] = ].b₁,b₃.]

proof end;

theorem Th13: :: RCOMP_2:13

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₁ <= b₃ & b₂ <= b₄ & b₃ <= b₄ holds
[.b₁,b₄.] = ([.b₁,b₂.[ \/ [.b₂,b₃.]) \/ ].b₃,b₄.]

proof end;

theorem Th14: :: RCOMP_2:14

for b₁, b₂, b₃, b₄ being real number st b₁ < b₂ & b₁ < b₃ & b₂ < b₄ & b₃ < b₄ holds
].b₁,b₄.[ = (].b₁,b₂.] \/ ].b₂,b₃.[) \/ [.b₃,b₄.[

proof end;

theorem Th15: :: RCOMP_2:15

for b₁, b₂, b₃, b₄ being real number holds [.b₁,b₂.[ /\ [.b₃,b₄.[ = [.(max b₁,b₃),(min b₂,b₄).[

proof end;

theorem Th16: :: RCOMP_2:16

for b₁, b₂, b₃, b₄ being real number holds ].b₁,b₂.] /\ ].b₃,b₄.] = ].(max b₁,b₃),(min b₂,b₄).]

proof end;

theorem Th17: :: RCOMP_2:17

for b₁, b₂ being real number holds
( ].b₁,b₂.[ c= [.b₁,b₂.[ & ].b₁,b₂.[ c= ].b₁,b₂.] & [.b₁,b₂.[ c= [.b₁,b₂.] & ].b₁,b₂.] c= [.b₁,b₂.] )

proof end;

theorem Th18: :: RCOMP_2:18

for b₁, b₂, b₃, b₄ being real number st b₁ in [.b₂,b₃.[ & b₄ in [.b₂,b₃.[ holds
[.b₁,b₄.] c= [.b₂,b₃.[

proof end;

theorem Th19: :: RCOMP_2:19

for b₁, b₂, b₃, b₄ being real number st b₁ in ].b₂,b₃.] & b₄ in ].b₂,b₃.] holds
[.b₁,b₄.] c= ].b₂,b₃.]

proof end;

theorem Th20: :: RCOMP_2:20

for b₁, b₂, b₃ being real number st b₁ <= b₂ & b₂ <= b₃ holds
[.b₁,b₂.] \/ ].b₂,b₃.] = [.b₁,b₃.]

proof end;

theorem Th21: :: RCOMP_2:21

for b₁, b₂, b₃ being real number st b₁ <= b₂ & b₂ <= b₃ holds
[.b₁,b₂.[ \/ [.b₂,b₃.] = [.b₁,b₃.]

proof end;

theorem Th22: :: RCOMP_2:22

for b₁, b₂, b₃, b₄ being real number st [.b₁,b₂.[ meets [.b₃,b₄.[ holds
b₂ >= b₃

proof end;

theorem Th23: :: RCOMP_2:23

for b₁, b₂, b₃, b₄ being real number st ].b₁,b₂.] meets ].b₃,b₄.] holds
b₂ >= b₃

proof end;

theorem Th24: :: RCOMP_2:24

for b₁, b₂, b₃, b₄ being real number st [.b₁,b₂.[ meets [.b₃,b₄.[ holds
[.b₁,b₂.[ \/ [.b₃,b₄.[ = [.(min b₁,b₃),(max b₂,b₄).[

proof end;

theorem Th25: :: RCOMP_2:25

for b₁, b₂, b₃, b₄ being real number st ].b₁,b₂.] meets ].b₃,b₄.] holds
].b₁,b₂.] \/ ].b₃,b₄.] = ].(min b₁,b₃),(max b₂,b₄).]

proof end;

theorem Th26: :: RCOMP_2:26

for b₁, b₂, b₃, b₄ being real number st [.b₁,b₂.[ meets [.b₃,b₄.[ holds
[.b₁,b₂.[ \ [.b₃,b₄.[ = [.b₁,b₃.[ \/ [.b₄,b₂.[

proof end;

theorem Th27: :: RCOMP_2:27

for b₁, b₂, b₃, b₄ being real number st ].b₁,b₂.] meets ].b₃,b₄.] holds
].b₁,b₂.] \ ].b₃,b₄.] = ].b₁,b₃.] \/ ].b₄,b₂.]

proof end;