:: RCOMP_2 semantic presentation

theorem :: RCOMP_2:1

canceled;

theorem Th2: :: RCOMP_2:2

for y, x, z being real number holds
( ( y < x & z < x ) iff max y,z < x )

proof end;

definition

let g, s be real number ;
func [.g,s.[ -> Subset of REAL equals :: RCOMP_2:def 1
{ r where r is Real : ( g <= r & r < s ) } ;
coherence

proof end;

func ].g,s.] -> Subset of REAL equals :: RCOMP_2:def 2
{ r where r is Real : ( g < r & r <= s ) } ;
coherence

proof end;

end;

:: deftheorem defines [. RCOMP_2:def 1 :

:: deftheorem defines ]. RCOMP_2:def 2 :

theorem Th3: :: RCOMP_2:3

for r, p, q being real number holds
( r in [.p,q.[ iff ( p <= r & r < q ) )

proof end;

theorem Th4: :: RCOMP_2:4

for r, p, q being real number holds
( r in ].p,q.] iff ( p < r & r <= q ) )

proof end;

theorem :: RCOMP_2:5

for g, s being real number st g < s holds
[.g,s.[ = ].g,s.[ \/ {g}

proof end;

theorem :: RCOMP_2:6

for g, s being real number st g < s holds
].g,s.] = ].g,s.[ \/ {s}

proof end;

theorem :: RCOMP_2:7

for g being real number holds [.g,g.[ = {}

proof end;

theorem :: RCOMP_2:8

for g being real number holds ].g,g.] = {}

proof end;

theorem :: RCOMP_2:9

for p, g being real number st p <= g holds
[.g,p.[ = {}

proof end;

theorem :: RCOMP_2:10

for p, g being real number st p <= g holds
].g,p.] = {}

proof end;

theorem :: RCOMP_2:11

for g, p, h being real number st g <= p & p <= h holds
[.g,p.[ \/ [.p,h.[ = [.g,h.[

proof end;

theorem :: RCOMP_2:12

for g, p, h being real number st g <= p & p <= h holds
].g,p.] \/ ].p,h.] = ].g,h.]

proof end;

theorem :: RCOMP_2:13

for g, p1, p2, h being real number st g <= p1 & g <= p2 & p1 <= h & p2 <= h holds
[.g,h.] = ([.g,p1.[ \/ [.p1,p2.]) \/ ].p2,h.]

proof end;

theorem :: RCOMP_2:14

for g, p1, p2, h being real number st g < p1 & g < p2 & p1 < h & p2 < h holds
].g,h.[ = (].g,p1.] \/ ].p1,p2.[) \/ [.p2,h.[

proof end;

theorem :: RCOMP_2:15

for q1, q2, p1, p2 being real number holds [.q1,q2.[ /\ [.p1,p2.[ = [.(max q1,p1),(min q2,p2).[

proof end;

theorem :: RCOMP_2:16

for q1, q2, p1, p2 being real number holds ].q1,q2.] /\ ].p1,p2.] = ].(max q1,p1),(min q2,p2).]

proof end;

theorem :: RCOMP_2:17

for p, q being real number holds
( ].p,q.[ c= [.p,q.[ & ].p,q.[ c= ].p,q.] & [.p,q.[ c= [.p,q.] & ].p,q.] c= [.p,q.] )

proof end;

theorem :: RCOMP_2:18

for r, p, g, s being real number st r in [.p,g.[ & s in [.p,g.[ holds
[.r,s.] c= [.p,g.[

proof end;

theorem :: RCOMP_2:19

for r, p, g, s being real number st r in ].p,g.] & s in ].p,g.] holds
[.r,s.] c= ].p,g.]

proof end;

theorem :: RCOMP_2:20

for p, q, r being real number st p <= q & q <= r holds
[.p,q.] \/ ].q,r.] = [.p,r.]

proof end;

theorem :: RCOMP_2:21

for p, q, r being real number st p <= q & q <= r holds
[.p,q.[ \/ [.q,r.] = [.p,r.]

proof end;

theorem Th22: :: RCOMP_2:22

for q1, q2, p1, p2 being real number st [.q1,q2.[ meets [.p1,p2.[ holds
q2 >= p1

proof end;

theorem Th23: :: RCOMP_2:23

for q1, q2, p1, p2 being real number st ].q1,q2.] meets ].p1,p2.] holds
q2 >= p1

proof end;

theorem :: RCOMP_2:24

for q1, q2, p1, p2 being real number st [.q1,q2.[ meets [.p1,p2.[ holds
[.q1,q2.[ \/ [.p1,p2.[ = [.(min q1,p1),(max q2,p2).[

proof end;

theorem :: RCOMP_2:25

for q1, q2, p1, p2 being real number st ].q1,q2.] meets ].p1,p2.] holds
].q1,q2.] \/ ].p1,p2.] = ].(min q1,p1),(max q2,p2).]

proof end;

theorem :: RCOMP_2:26

for p1, p2, q1, q2 being real number st [.p1,p2.[ meets [.q1,q2.[ holds
[.p1,p2.[ \ [.q1,q2.[ = [.p1,q1.[ \/ [.q2,p2.[

proof end;

theorem :: RCOMP_2:27

for p1, p2, q1, q2 being real number st ].p1,p2.] meets ].q1,q2.] holds
].p1,p2.] \ ].q1,q2.] = ].p1,q1.] \/ ].q2,p2.]

proof end;