:: by Yatsuka Nakamura and Czes\law Byli\'nski

::

:: Received May 11, 1994

:: Copyright (c) 1994 Association of Mizar Users

begin

theorem :: SPPOL_1:1

canceled;

theorem :: SPPOL_1:2

canceled;

theorem :: SPPOL_1:3

canceled;

theorem :: SPPOL_1:4

canceled;

theorem :: SPPOL_1:5

canceled;

theorem :: SPPOL_1:6

proof end;

theorem :: SPPOL_1:7

for k, m, n being Element of NAT st 1 <= k - m & k - m <= n holds

( k - m in Seg n & k - m is Element of NAT )

( k - m in Seg n & k - m is Element of NAT )

proof end;

scheme :: SPPOL_1:sch 1

FinSeqFam{ F_{1}() -> non empty set , F_{2}() -> FinSequence of F_{1}(), F_{3}( FinSequence of F_{1}(), Element of NAT ) -> set , P_{1}[ Nat] } :

FinSeqFam{ F

proof end;

scheme :: SPPOL_1:sch 2

FinSeqFam9{ F_{1}() -> non empty set , F_{2}() -> FinSequence of F_{1}(), F_{3}( FinSequence of F_{1}(), Element of NAT ) -> set , P_{1}[ set ] } :

FinSeqFam9{ F

proof end;

theorem :: SPPOL_1:8

canceled;

theorem :: SPPOL_1:9

canceled;

theorem :: SPPOL_1:10

canceled;

theorem :: SPPOL_1:11

canceled;

theorem :: SPPOL_1:12

canceled;

theorem :: SPPOL_1:13

canceled;

theorem :: SPPOL_1:14

canceled;

theorem Th15: :: SPPOL_1:15

for n being Element of NAT

for x1, x2, x3 being Element of REAL n holds |.(x1 - x2).| - |.(x2 - x3).| <= |.(x1 - x3).|

for x1, x2, x3 being Element of REAL n holds |.(x1 - x2).| - |.(x2 - x3).| <= |.(x1 - x3).|

proof end;

theorem :: SPPOL_1:16

for n being Element of NAT

for x1, x2, x3 being Element of REAL n holds |.(x2 - x1).| - |.(x2 - x3).| <= |.(x3 - x1).|

for x1, x2, x3 being Element of REAL n holds |.(x2 - x1).| - |.(x2 - x3).| <= |.(x3 - x1).|

proof end;

begin

theorem :: SPPOL_1:17

canceled;

theorem :: SPPOL_1:18

canceled;

theorem :: SPPOL_1:19

canceled;

theorem Th20: :: SPPOL_1:20

for n being Element of NAT

for u1, u2 being Point of (Euclid n)

for v1, v2 being Element of REAL n st v1 = u1 & v2 = u2 holds

dist (u1,u2) = |.(v1 - v2).|

for u1, u2 being Point of (Euclid n)

for v1, v2 being Element of REAL n st v1 = u1 & v2 = u2 holds

dist (u1,u2) = |.(v1 - v2).|

proof end;

theorem :: SPPOL_1:21

canceled;

theorem :: SPPOL_1:22

canceled;

theorem :: SPPOL_1:23

for n being Element of NAT

for p1, p2 being Point of (TOP-REAL n)

for P being non empty Subset of (TOP-REAL n) st P is closed & P c= LSeg (p1,p2) holds

ex s being Real st

( ((1 - s) * p1) + (s * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds

s <= r ) )

for p1, p2 being Point of (TOP-REAL n)

for P being non empty Subset of (TOP-REAL n) st P is closed & P c= LSeg (p1,p2) holds

ex s being Real st

( ((1 - s) * p1) + (s * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds

s <= r ) )

proof end;

theorem Th24: :: SPPOL_1:24

for n being Element of NAT

for p1, p2, q1, q2 being Point of (TOP-REAL n) st LSeg (q1,q2) c= LSeg (p1,p2) & p1 in LSeg (q1,q2) & not p1 = q1 holds

p1 = q2

for p1, p2, q1, q2 being Point of (TOP-REAL n) st LSeg (q1,q2) c= LSeg (p1,p2) & p1 in LSeg (q1,q2) & not p1 = q1 holds

p1 = q2

proof end;

theorem :: SPPOL_1:25

for n being Element of NAT

for p1, p2, q1, q2 being Point of (TOP-REAL n) holds

( not LSeg (p1,p2) = LSeg (q1,q2) or ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) )

for p1, p2, q1, q2 being Point of (TOP-REAL n) holds

( not LSeg (p1,p2) = LSeg (q1,q2) or ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) )

proof end;

theorem :: SPPOL_1:26

canceled;

theorem :: SPPOL_1:27

canceled;

theorem :: SPPOL_1:28

canceled;

theorem :: SPPOL_1:29

canceled;

registration

let n be Element of NAT ;

let p1, p2 be Point of (TOP-REAL n);

cluster LSeg (p1,p2) -> compact ;

coherence

LSeg (p1,p2) is compact

coherence

LSeg (p1,p2) is closed by COMPTS_1:16;

end;
let p1, p2 be Point of (TOP-REAL n);

cluster LSeg (p1,p2) -> compact ;

coherence

LSeg (p1,p2) is compact

proof end;

cluster LSeg (p1,p2) -> closed ;coherence

LSeg (p1,p2) is closed by COMPTS_1:16;

definition

let n be Element of NAT ;

let p be Point of (TOP-REAL n);

let P be Subset of (TOP-REAL n);

pred p is_extremal_in P means :Def1: :: SPPOL_1:def 1

( p in P & ( for p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) & LSeg (p1,p2) c= P & not p = p1 holds

p = p2 ) );

end;
let p be Point of (TOP-REAL n);

let P be Subset of (TOP-REAL n);

pred p is_extremal_in P means :Def1: :: SPPOL_1:def 1

( p in P & ( for p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) & LSeg (p1,p2) c= P & not p = p1 holds

p = p2 ) );

:: deftheorem Def1 defines is_extremal_in SPPOL_1:def 1 :

for n being Element of NAT

for p being Point of (TOP-REAL n)

for P being Subset of (TOP-REAL n) holds

( p is_extremal_in P iff ( p in P & ( for p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) & LSeg (p1,p2) c= P & not p = p1 holds

p = p2 ) ) );

theorem :: SPPOL_1:30

for n being Element of NAT

for p being Point of (TOP-REAL n)

for P, Q being Subset of (TOP-REAL n) st p is_extremal_in P & Q c= P & p in Q holds

p is_extremal_in Q

for p being Point of (TOP-REAL n)

for P, Q being Subset of (TOP-REAL n) st p is_extremal_in P & Q c= P & p in Q holds

p is_extremal_in Q

proof end;

theorem :: SPPOL_1:31

proof end;

theorem Th32: :: SPPOL_1:32

for n being Element of NAT

for p1, p2 being Point of (TOP-REAL n) holds p1 is_extremal_in LSeg (p1,p2)

for p1, p2 being Point of (TOP-REAL n) holds p1 is_extremal_in LSeg (p1,p2)

proof end;

theorem :: SPPOL_1:33

for n being Element of NAT

for p2, p1 being Point of (TOP-REAL n) holds p2 is_extremal_in LSeg (p1,p2) by Th32;

for p2, p1 being Point of (TOP-REAL n) holds p2 is_extremal_in LSeg (p1,p2) by Th32;

theorem :: SPPOL_1:34

for n being Element of NAT

for p, p1, p2 being Point of (TOP-REAL n) holds

( not p is_extremal_in LSeg (p1,p2) or p = p1 or p = p2 )

for p, p1, p2 being Point of (TOP-REAL n) holds

( not p is_extremal_in LSeg (p1,p2) or p = p1 or p = p2 )

proof end;

begin

theorem Th35: :: SPPOL_1:35

for p1, p2 being Point of (TOP-REAL 2) st p1 `1 <> p2 `1 & p1 `2 <> p2 `2 holds

ex p being Point of (TOP-REAL 2) st

( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 )

ex p being Point of (TOP-REAL 2) st

( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 )

proof end;

definition

let P be Subset of (TOP-REAL 2);

attr P is horizontal means :Def2: :: SPPOL_1:def 2

for p, q being Point of (TOP-REAL 2) st p in P & q in P holds

p `2 = q `2 ;

attr P is vertical means :Def3: :: SPPOL_1:def 3

for p, q being Point of (TOP-REAL 2) st p in P & q in P holds

p `1 = q `1 ;

end;
attr P is horizontal means :Def2: :: SPPOL_1:def 2

for p, q being Point of (TOP-REAL 2) st p in P & q in P holds

p `2 = q `2 ;

attr P is vertical means :Def3: :: SPPOL_1:def 3

for p, q being Point of (TOP-REAL 2) st p in P & q in P holds

p `1 = q `1 ;

:: deftheorem Def2 defines horizontal SPPOL_1:def 2 :

for P being Subset of (TOP-REAL 2) holds

( P is horizontal iff for p, q being Point of (TOP-REAL 2) st p in P & q in P holds

p `2 = q `2 );

:: deftheorem Def3 defines vertical SPPOL_1:def 3 :

for P being Subset of (TOP-REAL 2) holds

( P is vertical iff for p, q being Point of (TOP-REAL 2) st p in P & q in P holds

p `1 = q `1 );

Lm1: for P being Subset of (TOP-REAL 2) st not P is trivial & P is horizontal holds

not P is vertical

proof end;

registration

cluster non trivial horizontal -> non vertical Element of K10( the carrier of (TOP-REAL 2));

coherence

for b_{1} being Subset of (TOP-REAL 2) st not b_{1} is trivial & b_{1} is horizontal holds

not b_{1} is vertical
by Lm1;

cluster non trivial vertical -> non horizontal Element of K10( the carrier of (TOP-REAL 2));

coherence

for b_{1} being Subset of (TOP-REAL 2) st not b_{1} is trivial & b_{1} is vertical holds

not b_{1} is horizontal
;

end;
coherence

for b

not b

cluster non trivial vertical -> non horizontal Element of K10( the carrier of (TOP-REAL 2));

coherence

for b

not b

theorem Th36: :: SPPOL_1:36

proof end;

theorem Th37: :: SPPOL_1:37

proof end;

theorem :: SPPOL_1:38

for p1, p, q, p2 being Point of (TOP-REAL 2) st p1 in LSeg (p,q) & p2 in LSeg (p,q) & p1 `1 <> p2 `1 & p1 `2 = p2 `2 holds

LSeg (p,q) is horizontal

LSeg (p,q) is horizontal

proof end;

theorem :: SPPOL_1:39

for p1, p, q, p2 being Point of (TOP-REAL 2) st p1 in LSeg (p,q) & p2 in LSeg (p,q) & p1 `2 <> p2 `2 & p1 `1 = p2 `1 holds

LSeg (p,q) is vertical

LSeg (p,q) is vertical

proof end;

theorem :: SPPOL_1:40

canceled;

registration

let f be FinSequence of the carrier of (TOP-REAL 2);

let i be Element of NAT ;

cluster LSeg (f,i) -> closed ;

coherence

LSeg (f,i) is closed

end;
let i be Element of NAT ;

cluster LSeg (f,i) -> closed ;

coherence

LSeg (f,i) is closed

proof end;

theorem Th41: :: SPPOL_1:41

for i being Element of NAT

for f being FinSequence of the carrier of (TOP-REAL 2) holds

( not f is special or LSeg (f,i) is vertical or LSeg (f,i) is horizontal )

for f being FinSequence of the carrier of (TOP-REAL 2) holds

( not f is special or LSeg (f,i) is vertical or LSeg (f,i) is horizontal )

proof end;

theorem Th42: :: SPPOL_1:42

for i being Element of NAT

for f being FinSequence of the carrier of (TOP-REAL 2) st f is one-to-one & 1 <= i & i + 1 <= len f holds

not LSeg (f,i) is trivial

for f being FinSequence of the carrier of (TOP-REAL 2) st f is one-to-one & 1 <= i & i + 1 <= len f holds

not LSeg (f,i) is trivial

proof end;

theorem :: SPPOL_1:43

for i being Element of NAT

for f being FinSequence of the carrier of (TOP-REAL 2) st f is one-to-one & 1 <= i & i + 1 <= len f & LSeg (f,i) is vertical holds

not LSeg (f,i) is horizontal by Lm1, Th42;

for f being FinSequence of the carrier of (TOP-REAL 2) st f is one-to-one & 1 <= i & i + 1 <= len f & LSeg (f,i) is vertical holds

not LSeg (f,i) is horizontal by Lm1, Th42;

theorem Th44: :: SPPOL_1:44

for f being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } is finite

proof end;

theorem Th45: :: SPPOL_1:45

for f being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } is finite

proof end;

Lm2: for f being FinSequence of the carrier of (TOP-REAL 2)

for k being Element of NAT holds { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is finite

proof end;

theorem :: SPPOL_1:46

for f being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } is Subset-Family of (TOP-REAL 2)

proof end;

theorem Th47: :: SPPOL_1:47

for f being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } is Subset-Family of (TOP-REAL 2)

proof end;

Lm3: for f being FinSequence of the carrier of (TOP-REAL 2)

for k being Element of NAT holds { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is Subset-Family of (TOP-REAL 2)

proof end;

theorem Th48: :: SPPOL_1:48

for Q being Subset of (TOP-REAL 2)

for f being FinSequence of the carrier of (TOP-REAL 2) st Q = union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } holds

Q is closed

for f being FinSequence of the carrier of (TOP-REAL 2) st Q = union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } holds

Q is closed

proof end;

theorem :: SPPOL_1:49

canceled;

registration

let f be FinSequence of the carrier of (TOP-REAL 2);

cluster L~ f -> closed ;

coherence

L~ f is closed by Th48;

end;
cluster L~ f -> closed ;

coherence

L~ f is closed by Th48;

Lm4: for f being FinSequence of the carrier of (TOP-REAL 2)

for Q being Subset of (TOP-REAL 2)

for k being Element of NAT st Q = union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } holds

Q is closed

proof end;

definition

let IT be FinSequence of (TOP-REAL 2);

attr IT is alternating means :Def4: :: SPPOL_1:def 4

for i being Element of NAT st 1 <= i & i + 2 <= len IT holds

( (IT /. i) `1 <> (IT /. (i + 2)) `1 & (IT /. i) `2 <> (IT /. (i + 2)) `2 );

end;
attr IT is alternating means :Def4: :: SPPOL_1:def 4

for i being Element of NAT st 1 <= i & i + 2 <= len IT holds

( (IT /. i) `1 <> (IT /. (i + 2)) `1 & (IT /. i) `2 <> (IT /. (i + 2)) `2 );

:: deftheorem Def4 defines alternating SPPOL_1:def 4 :

for IT being FinSequence of (TOP-REAL 2) holds

( IT is alternating iff for i being Element of NAT st 1 <= i & i + 2 <= len IT holds

( (IT /. i) `1 <> (IT /. (i + 2)) `1 & (IT /. i) `2 <> (IT /. (i + 2)) `2 ) );

theorem Th50: :: SPPOL_1:50

for i being Element of NAT

for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & (f /. i) `1 = (f /. (i + 1)) `1 holds

(f /. (i + 1)) `2 = (f /. (i + 2)) `2

for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & (f /. i) `1 = (f /. (i + 1)) `1 holds

(f /. (i + 1)) `2 = (f /. (i + 2)) `2

proof end;

theorem Th51: :: SPPOL_1:51

for i being Element of NAT

for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & (f /. i) `2 = (f /. (i + 1)) `2 holds

(f /. (i + 1)) `1 = (f /. (i + 2)) `1

for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & (f /. i) `2 = (f /. (i + 1)) `2 holds

(f /. (i + 1)) `1 = (f /. (i + 2)) `1

proof end;

theorem Th52: :: SPPOL_1:52

for i being Element of NAT

for f being FinSequence of the carrier of (TOP-REAL 2)

for p1, p2, p3 being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 1) & p3 = f /. (i + 2) & not ( p1 `1 = p2 `1 & p3 `1 <> p2 `1 ) holds

( p1 `2 = p2 `2 & p3 `2 <> p2 `2 )

for f being FinSequence of the carrier of (TOP-REAL 2)

for p1, p2, p3 being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 1) & p3 = f /. (i + 2) & not ( p1 `1 = p2 `1 & p3 `1 <> p2 `1 ) holds

( p1 `2 = p2 `2 & p3 `2 <> p2 `2 )

proof end;

theorem :: SPPOL_1:53

for i being Element of NAT

for f being FinSequence of the carrier of (TOP-REAL 2)

for p1, p2, p3 being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 1) & p3 = f /. (i + 2) & not ( p2 `1 = p3 `1 & p1 `1 <> p2 `1 ) holds

( p2 `2 = p3 `2 & p1 `2 <> p2 `2 )

for f being FinSequence of the carrier of (TOP-REAL 2)

for p1, p2, p3 being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 1) & p3 = f /. (i + 2) & not ( p2 `1 = p3 `1 & p1 `1 <> p2 `1 ) holds

( p2 `2 = p3 `2 & p1 `2 <> p2 `2 )

proof end;

Lm5: for f being FinSequence of the carrier of (TOP-REAL 2)

for i being Element of NAT

for p1, p2 being Point of (TOP-REAL 2) st f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 2) holds

ex p being Point of (TOP-REAL 2) st

( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 )

proof end;

theorem :: SPPOL_1:54

for i being Element of NAT

for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f holds

not LSeg ((f /. i),(f /. (i + 2))) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1)))

for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f holds

not LSeg ((f /. i),(f /. (i + 2))) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1)))

proof end;

theorem Th55: :: SPPOL_1:55

for i being Element of NAT

for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & LSeg (f,i) is vertical holds

LSeg (f,(i + 1)) is horizontal

for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & LSeg (f,i) is vertical holds

LSeg (f,(i + 1)) is horizontal

proof end;

theorem Th56: :: SPPOL_1:56

for i being Element of NAT

for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & LSeg (f,i) is horizontal holds

LSeg (f,(i + 1)) is vertical

for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & LSeg (f,i) is horizontal holds

LSeg (f,(i + 1)) is vertical

proof end;

theorem :: SPPOL_1:57

for i being Element of NAT

for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & not ( LSeg (f,i) is vertical & LSeg (f,(i + 1)) is horizontal ) holds

( LSeg (f,i) is horizontal & LSeg (f,(i + 1)) is vertical )

for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & not ( LSeg (f,i) is vertical & LSeg (f,(i + 1)) is horizontal ) holds

( LSeg (f,i) is horizontal & LSeg (f,(i + 1)) is vertical )

proof end;

theorem Th58: :: SPPOL_1:58

for i being Element of NAT

for f being FinSequence of the carrier of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & f /. (i + 1) in LSeg (p,q) & LSeg (p,q) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & not f /. (i + 1) = p holds

f /. (i + 1) = q

for f being FinSequence of the carrier of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & f /. (i + 1) in LSeg (p,q) & LSeg (p,q) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & not f /. (i + 1) = p holds

f /. (i + 1) = q

proof end;

theorem Th59: :: SPPOL_1:59

for i being Element of NAT

for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f holds

f /. (i + 1) is_extremal_in (LSeg (f,i)) \/ (LSeg (f,(i + 1)))

for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f holds

f /. (i + 1) is_extremal_in (LSeg (f,i)) \/ (LSeg (f,(i + 1)))

proof end;

theorem Th60: :: SPPOL_1:60

for i being Element of NAT

for f being FinSequence of the carrier of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2)

for u being Point of (Euclid 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & u = f /. (i + 1) & f /. (i + 1) in LSeg (p,q) & f /. (i + 1) <> q & not p in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) holds

for s being Real st s > 0 holds

ex p3 being Point of (TOP-REAL 2) st

( not p3 in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & p3 in LSeg (p,q) & p3 in Ball (u,s) )

for f being FinSequence of the carrier of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2)

for u being Point of (Euclid 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & u = f /. (i + 1) & f /. (i + 1) in LSeg (p,q) & f /. (i + 1) <> q & not p in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) holds

for s being Real st s > 0 holds

ex p3 being Point of (TOP-REAL 2) st

( not p3 in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & p3 in LSeg (p,q) & p3 in Ball (u,s) )

proof end;

definition

let f1, f2 be FinSequence of the carrier of (TOP-REAL 2);

let P be Subset of (TOP-REAL 2);

pred f1,f2 are_generators_of P means :Def5: :: SPPOL_1:def 5

( f1 is alternating & f1 is being_S-Seq & f2 is alternating & f2 is being_S-Seq & f1 /. 1 = f2 /. 1 & f1 /. (len f1) = f2 /. (len f2) & <*(f1 /. 2),(f1 /. 1),(f2 /. 2)*> is alternating & <*(f1 /. ((len f1) - 1)),(f1 /. (len f1)),(f2 /. ((len f2) - 1))*> is alternating & f1 /. 1 <> f1 /. (len f1) & (L~ f1) /\ (L~ f2) = {(f1 /. 1),(f1 /. (len f1))} & P = (L~ f1) \/ (L~ f2) );

end;
let P be Subset of (TOP-REAL 2);

pred f1,f2 are_generators_of P means :Def5: :: SPPOL_1:def 5

( f1 is alternating & f1 is being_S-Seq & f2 is alternating & f2 is being_S-Seq & f1 /. 1 = f2 /. 1 & f1 /. (len f1) = f2 /. (len f2) & <*(f1 /. 2),(f1 /. 1),(f2 /. 2)*> is alternating & <*(f1 /. ((len f1) - 1)),(f1 /. (len f1)),(f2 /. ((len f2) - 1))*> is alternating & f1 /. 1 <> f1 /. (len f1) & (L~ f1) /\ (L~ f2) = {(f1 /. 1),(f1 /. (len f1))} & P = (L~ f1) \/ (L~ f2) );

:: deftheorem Def5 defines are_generators_of SPPOL_1:def 5 :

for f1, f2 being FinSequence of the carrier of (TOP-REAL 2)

for P being Subset of (TOP-REAL 2) holds

( f1,f2 are_generators_of P iff ( f1 is alternating & f1 is being_S-Seq & f2 is alternating & f2 is being_S-Seq & f1 /. 1 = f2 /. 1 & f1 /. (len f1) = f2 /. (len f2) & <*(f1 /. 2),(f1 /. 1),(f2 /. 2)*> is alternating & <*(f1 /. ((len f1) - 1)),(f1 /. (len f1)),(f2 /. ((len f2) - 1))*> is alternating & f1 /. 1 <> f1 /. (len f1) & (L~ f1) /\ (L~ f2) = {(f1 /. 1),(f1 /. (len f1))} & P = (L~ f1) \/ (L~ f2) ) );

theorem :: SPPOL_1:61

for i being Element of NAT

for P being Subset of (TOP-REAL 2)

for f1, f2 being FinSequence of the carrier of (TOP-REAL 2) st f1,f2 are_generators_of P & 1 < i & i < len f1 holds

f1 /. i is_extremal_in P

for P being Subset of (TOP-REAL 2)

for f1, f2 being FinSequence of the carrier of (TOP-REAL 2) st f1,f2 are_generators_of P & 1 < i & i < len f1 holds

f1 /. i is_extremal_in P

proof end;

theorem :: SPPOL_1:62

for n being Element of NAT

for p, q being Point of (TOP-REAL n)

for p9, q9 being Point of (Euclid n) st p = p9 & q = q9 holds

dist (p9,q9) = |.(p - q).|

for p, q being Point of (TOP-REAL n)

for p9, q9 being Point of (Euclid n) st p = p9 & q = q9 holds

dist (p9,q9) = |.(p - q).|

proof end;

theorem :: SPPOL_1:63

for p, q, r being Point of (TOP-REAL 2) st LSeg (p,q) is horizontal & r in LSeg (p,q) holds

p `2 = r `2

p `2 = r `2

proof end;

theorem :: SPPOL_1:64

for p, q, r being Point of (TOP-REAL 2) st LSeg (p,q) is vertical & r in LSeg (p,q) holds

p `1 = r `1

p `1 = r `1

proof end;

registration

cluster non empty compact horizontal Element of K10( the carrier of (TOP-REAL 2));

existence

ex b_{1} being Subset of (TOP-REAL 2) st

( b_{1} is compact & not b_{1} is empty & b_{1} is horizontal )

existence

ex b_{1} being Subset of (TOP-REAL 2) st

( b_{1} is compact & not b_{1} is empty & b_{1} is vertical )

end;
existence

ex b

( b

proof end;

cluster non empty compact vertical Element of K10( the carrier of (TOP-REAL 2));existence

ex b

( b

proof end;