:: by Agata Darmochwa{\l} and Yatsuka Nakamura

::

:: Received November 21, 1991

:: Copyright (c) 1991-2012 Association of Mizar Users

begin

:: PRELIMINARIES

definition

let T be TopSpace;

let p1, p2 be Point of T;

let P be Subset of T;

end;
let p1, p2 be Point of T;

let P be Subset of T;

pred P is_an_arc_of p1,p2 means :Def1: :: TOPREAL1:def 1

ex f being Function of I[01],(T | P) st

( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 );

ex f being Function of I[01],(T | P) st

( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 );

:: deftheorem Def1 defines is_an_arc_of TOPREAL1:def 1 :

for T being TopSpace

for p1, p2 being Point of T

for P being Subset of T holds

( P is_an_arc_of p1,p2 iff ex f being Function of I[01],(T | P) st

( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) );

for T being TopSpace

for p1, p2 being Point of T

for P being Subset of T holds

( P is_an_arc_of p1,p2 iff ex f being Function of I[01],(T | P) st

( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) );

theorem Th1: :: TOPREAL1:1

for T being TopSpace

for P being Subset of T

for p1, p2 being Point of T st P is_an_arc_of p1,p2 holds

( p1 in P & p2 in P )

for P being Subset of T

for p1, p2 being Point of T st P is_an_arc_of p1,p2 holds

( p1 in P & p2 in P )

proof end;

theorem Th2: :: TOPREAL1:2

for T being T_2 TopSpace

for P, Q being Subset of T

for p1, p2, q1 being Point of T st P is_an_arc_of p1,p2 & Q is_an_arc_of p2,q1 & P /\ Q = {p2} holds

P \/ Q is_an_arc_of p1,q1

for P, Q being Subset of T

for p1, p2, q1 being Point of T st P is_an_arc_of p1,p2 & Q is_an_arc_of p2,q1 & P /\ Q = {p2} holds

P \/ Q is_an_arc_of p1,q1

proof end;

definition

((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|))) is Subset of (TOP-REAL 2) ;

end;

func R^2-unit_square -> Subset of (TOP-REAL 2) equals :: TOPREAL1:def 2

((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|)));

coherence ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|)));

((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|))) is Subset of (TOP-REAL 2) ;

:: deftheorem defines R^2-unit_square TOPREAL1:def 2 :

R^2-unit_square = ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|)));

R^2-unit_square = ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|)));

Lm1: for n being Nat

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

LSeg (p1,p) c= LSeg (p1,p2)

proof end;

theorem :: TOPREAL1:3

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

( p1 `1 <= p `1 & p `1 <= p2 `1 )

( p1 `1 <= p `1 & p `1 <= p2 `1 )

proof end;

theorem :: TOPREAL1:4

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

( p1 `2 <= p `2 & p `2 <= p2 `2 )

( p1 `2 <= p `2 & p `2 <= p2 `2 )

proof end;

theorem Th5: :: TOPREAL1:5

for n being Nat

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

LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2))

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

LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2))

proof end;

theorem Th6: :: TOPREAL1:6

for n being Nat

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

LSeg (q1,q2) c= LSeg (p1,p2)

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

LSeg (q1,q2) c= LSeg (p1,p2)

proof end;

theorem :: TOPREAL1:7

for n being Nat

for p, q, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) & q in LSeg (p1,p2) holds

LSeg (p1,p2) = ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2))

for p, q, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) & q in LSeg (p1,p2) holds

LSeg (p1,p2) = ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2))

proof end;

theorem :: TOPREAL1:8

for n being Nat

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

(LSeg (p1,p)) /\ (LSeg (p,p2)) = {p}

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

(LSeg (p1,p)) /\ (LSeg (p,p2)) = {p}

proof end;

Lm2: for T being TopSpace holds

( T is T_2 iff TopStruct(# the carrier of T, the topology of T #) is T_2 )

proof end;

theorem Th9: :: TOPREAL1:9

for n being Nat

for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds

LSeg (p1,p2) is_an_arc_of p1,p2

for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds

LSeg (p1,p2) is_an_arc_of p1,p2

proof end;

theorem Th10: :: TOPREAL1:10

for n being Nat

for P being Subset of (TOP-REAL n)

for p1, p2, q1 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & P /\ (LSeg (p2,q1)) = {p2} holds

P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1

for P being Subset of (TOP-REAL n)

for p1, p2, q1 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & P /\ (LSeg (p2,q1)) = {p2} holds

P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1

proof end;

theorem Th11: :: TOPREAL1:11

for n being Nat

for P being Subset of (TOP-REAL n)

for p1, p2, q1 being Point of (TOP-REAL n) st P is_an_arc_of p2,p1 & (LSeg (q1,p2)) /\ P = {p2} holds

(LSeg (q1,p2)) \/ P is_an_arc_of q1,p1

for P being Subset of (TOP-REAL n)

for p1, p2, q1 being Point of (TOP-REAL n) st P is_an_arc_of p2,p1 & (LSeg (q1,p2)) /\ P = {p2} holds

(LSeg (q1,p2)) \/ P is_an_arc_of q1,p1

proof end;

theorem :: TOPREAL1:12

for n being Nat

for p1, p2, q1 being Point of (TOP-REAL n) st ( p1 <> p2 or p2 <> q1 ) & (LSeg (p1,p2)) /\ (LSeg (p2,q1)) = {p2} holds

(LSeg (p1,p2)) \/ (LSeg (p2,q1)) is_an_arc_of p1,q1

for p1, p2, q1 being Point of (TOP-REAL n) st ( p1 <> p2 or p2 <> q1 ) & (LSeg (p1,p2)) /\ (LSeg (p2,q1)) = {p2} holds

(LSeg (p1,p2)) \/ (LSeg (p2,q1)) is_an_arc_of p1,q1

proof end;

theorem Th13: :: TOPREAL1:13

( LSeg (|[0,0]|,|[0,1]|) = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = 0 & p1 `2 <= 1 & p1 `2 >= 0 ) } & LSeg (|[0,1]|,|[1,1]|) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 1 ) } & LSeg (|[0,0]|,|[1,0]|) = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= 1 & q1 `1 >= 0 & q1 `2 = 0 ) } & LSeg (|[1,0]|,|[1,1]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = 1 & q2 `2 <= 1 & q2 `2 >= 0 ) } )

proof end;

theorem :: TOPREAL1:14

R^2-unit_square = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) or ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) ) }

proof end;

definition

let n be Nat;

let f be FinSequence of (TOP-REAL n);

let i be Nat;

( ( 1 <= i & i + 1 <= len f implies LSeg ((f /. i),(f /. (i + 1))) is Subset of (TOP-REAL n) ) & ( ( not 1 <= i or not i + 1 <= len f ) implies {} is Subset of (TOP-REAL n) ) )

consistency

for b_{1} being Subset of (TOP-REAL n) holds verum;

;

end;
let f be FinSequence of (TOP-REAL n);

let i be Nat;

func LSeg (f,i) -> Subset of (TOP-REAL n) equals :Def3: :: TOPREAL1:def 3

LSeg ((f /. i),(f /. (i + 1))) if ( 1 <= i & i + 1 <= len f )

otherwise {} ;

coherence LSeg ((f /. i),(f /. (i + 1))) if ( 1 <= i & i + 1 <= len f )

otherwise {} ;

( ( 1 <= i & i + 1 <= len f implies LSeg ((f /. i),(f /. (i + 1))) is Subset of (TOP-REAL n) ) & ( ( not 1 <= i or not i + 1 <= len f ) implies {} is Subset of (TOP-REAL n) ) )

proof end;

correctness consistency

for b

;

:: deftheorem Def3 defines LSeg TOPREAL1:def 3 :

for n being Nat

for f being FinSequence of (TOP-REAL n)

for i being Nat holds

( ( 1 <= i & i + 1 <= len f implies LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) ) & ( ( not 1 <= i or not i + 1 <= len f ) implies LSeg (f,i) = {} ) );

for n being Nat

for f being FinSequence of (TOP-REAL n)

for i being Nat holds

( ( 1 <= i & i + 1 <= len f implies LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) ) & ( ( not 1 <= i or not i + 1 <= len f ) implies LSeg (f,i) = {} ) );

theorem Th21: :: TOPREAL1:21

for n, i being Nat

for f being FinSequence of (TOP-REAL n) st 1 <= i & i + 1 <= len f holds

( f /. i in LSeg (f,i) & f /. (i + 1) in LSeg (f,i) )

for f being FinSequence of (TOP-REAL n) st 1 <= i & i + 1 <= len f holds

( f /. i in LSeg (f,i) & f /. (i + 1) in LSeg (f,i) )

proof end;

definition

let n be Nat;

let f be FinSequence of (TOP-REAL n);

union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } is Subset of (TOP-REAL n)

end;
let f be FinSequence of (TOP-REAL n);

func L~ f -> Subset of (TOP-REAL n) equals :: TOPREAL1:def 4

union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;

coherence union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;

union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } is Subset of (TOP-REAL n)

proof end;

:: deftheorem defines L~ TOPREAL1:def 4 :

for n being Nat

for f being FinSequence of (TOP-REAL n) holds L~ f = union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;

for n being Nat

for f being FinSequence of (TOP-REAL n) holds L~ f = union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;

theorem Th22: :: TOPREAL1:22

for n being Nat

for f being FinSequence of (TOP-REAL n) holds

( ( len f = 0 or len f = 1 ) iff L~ f = {} )

for f being FinSequence of (TOP-REAL n) holds

( ( len f = 0 or len f = 1 ) iff L~ f = {} )

proof end;

definition

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

end;
attr IT is special means :: TOPREAL1:def 5

for i being Nat st 1 <= i & i + 1 <= len IT & not (IT /. i) `1 = (IT /. (i + 1)) `1 holds

(IT /. i) `2 = (IT /. (i + 1)) `2 ;

for i being Nat st 1 <= i & i + 1 <= len IT & not (IT /. i) `1 = (IT /. (i + 1)) `1 holds

(IT /. i) `2 = (IT /. (i + 1)) `2 ;

attr IT is unfolded means :Def6: :: TOPREAL1:def 6

for i being Nat st 1 <= i & i + 2 <= len IT holds

(LSeg (IT,i)) /\ (LSeg (IT,(i + 1))) = {(IT /. (i + 1))};

for i being Nat st 1 <= i & i + 2 <= len IT holds

(LSeg (IT,i)) /\ (LSeg (IT,(i + 1))) = {(IT /. (i + 1))};

:: deftheorem defines special TOPREAL1:def 5 :

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

( IT is special iff for i being Nat st 1 <= i & i + 1 <= len IT & not (IT /. i) `1 = (IT /. (i + 1)) `1 holds

(IT /. i) `2 = (IT /. (i + 1)) `2 );

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

( IT is special iff for i being Nat st 1 <= i & i + 1 <= len IT & not (IT /. i) `1 = (IT /. (i + 1)) `1 holds

(IT /. i) `2 = (IT /. (i + 1)) `2 );

:: deftheorem Def6 defines unfolded TOPREAL1:def 6 :

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

( IT is unfolded iff for i being Nat st 1 <= i & i + 2 <= len IT holds

(LSeg (IT,i)) /\ (LSeg (IT,(i + 1))) = {(IT /. (i + 1))} );

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

( IT is unfolded iff for i being Nat st 1 <= i & i + 2 <= len IT holds

(LSeg (IT,i)) /\ (LSeg (IT,(i + 1))) = {(IT /. (i + 1))} );

:: deftheorem Def7 defines s.n.c. TOPREAL1:def 7 :

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

( IT is s.n.c. iff for i, j being Nat st i + 1 < j holds

LSeg (IT,i) misses LSeg (IT,j) );

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

( IT is s.n.c. iff for i, j being Nat st i + 1 < j holds

LSeg (IT,i) misses LSeg (IT,j) );

definition

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

end;
attr f is being_S-Seq means :Def8: :: TOPREAL1:def 8

( f is one-to-one & len f >= 2 & f is unfolded & f is s.n.c. & f is special );

( f is one-to-one & len f >= 2 & f is unfolded & f is s.n.c. & f is special );

:: deftheorem Def8 defines being_S-Seq TOPREAL1:def 8 :

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

( f is being_S-Seq iff ( f is one-to-one & len f >= 2 & f is unfolded & f is s.n.c. & f is special ) );

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

( f is being_S-Seq iff ( f is one-to-one & len f >= 2 & f is unfolded & f is s.n.c. & f is special ) );

theorem Th24: :: TOPREAL1:24

ex f1, f2 being FinSequence of (TOP-REAL 2) st

( f1 is being_S-Seq & f2 is being_S-Seq & R^2-unit_square = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[0,0]|,|[1,1]|} & f1 /. 1 = |[0,0]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0,0]| & f2 /. (len f2) = |[1,1]| )

( f1 is being_S-Seq & f2 is being_S-Seq & R^2-unit_square = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[0,0]|,|[1,1]|} & f1 /. 1 = |[0,0]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0,0]| & f2 /. (len f2) = |[1,1]| )

proof end;

theorem Th25: :: TOPREAL1:25

for h being FinSequence of (TOP-REAL 2) st h is being_S-Seq holds

L~ h is_an_arc_of h /. 1,h /. (len h)

L~ h is_an_arc_of h /. 1,h /. (len h)

proof end;

definition

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

end;
attr P is being_S-P_arc means :Def9: :: TOPREAL1:def 9

ex f being FinSequence of (TOP-REAL 2) st

( f is being_S-Seq & P = L~ f );

ex f being FinSequence of (TOP-REAL 2) st

( f is being_S-Seq & P = L~ f );

:: deftheorem Def9 defines being_S-P_arc TOPREAL1:def 9 :

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

( P is being_S-P_arc iff ex f being FinSequence of (TOP-REAL 2) st

( f is being_S-Seq & P = L~ f ) );

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

( P is being_S-P_arc iff ex f being FinSequence of (TOP-REAL 2) st

( f is being_S-Seq & P = L~ f ) );

registration

coherence

for b_{1} being Subset of (TOP-REAL 2) st b_{1} is being_S-P_arc holds

not b_{1} is empty
by Th26;

end;
for b

not b

theorem :: TOPREAL1:27

ex P1, P2 being non empty Subset of (TOP-REAL 2) st

( P1 is being_S-P_arc & P2 is being_S-P_arc & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {|[0,0]|,|[1,1]|} )

( P1 is being_S-P_arc & P2 is being_S-P_arc & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {|[0,0]|,|[1,1]|} )

proof end;

theorem Th28: :: TOPREAL1:28

for P being Subset of (TOP-REAL 2) st P is being_S-P_arc holds

ex p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2

ex p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2

proof end;

theorem :: TOPREAL1:29

for P being Subset of (TOP-REAL 2) st P is being_S-P_arc holds

ex f being Function of I[01],((TOP-REAL 2) | P) st f is being_homeomorphism

ex f being Function of I[01],((TOP-REAL 2) | P) st f is being_homeomorphism

proof end;

:: Moved from JORDAN1A, AK, 23.02.2006

definition

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

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

for x being Point of (TOP-REAL 2) holds

( x in b_{1} iff ( x `1 = p `1 & x `2 >= p `2 ) )

for b_{1}, b_{2} being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds

( x in b_{1} iff ( x `1 = p `1 & x `2 >= p `2 ) ) ) & ( for x being Point of (TOP-REAL 2) holds

( x in b_{2} iff ( x `1 = p `1 & x `2 >= p `2 ) ) ) holds

b_{1} = b_{2}

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

for x being Point of (TOP-REAL 2) holds

( x in b_{1} iff ( x `1 >= p `1 & x `2 = p `2 ) )

for b_{1}, b_{2} being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds

( x in b_{1} iff ( x `1 >= p `1 & x `2 = p `2 ) ) ) & ( for x being Point of (TOP-REAL 2) holds

( x in b_{2} iff ( x `1 >= p `1 & x `2 = p `2 ) ) ) holds

b_{1} = b_{2}

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

for x being Point of (TOP-REAL 2) holds

( x in b_{1} iff ( x `1 = p `1 & x `2 <= p `2 ) )

for b_{1}, b_{2} being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds

( x in b_{1} iff ( x `1 = p `1 & x `2 <= p `2 ) ) ) & ( for x being Point of (TOP-REAL 2) holds

( x in b_{2} iff ( x `1 = p `1 & x `2 <= p `2 ) ) ) holds

b_{1} = b_{2}

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

for x being Point of (TOP-REAL 2) holds

( x in b_{1} iff ( x `1 <= p `1 & x `2 = p `2 ) )

for b_{1}, b_{2} being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds

( x in b_{1} iff ( x `1 <= p `1 & x `2 = p `2 ) ) ) & ( for x being Point of (TOP-REAL 2) holds

( x in b_{2} iff ( x `1 <= p `1 & x `2 = p `2 ) ) ) holds

b_{1} = b_{2}

end;
func north_halfline p -> Subset of (TOP-REAL 2) means :Def10: :: TOPREAL1:def 10

for x being Point of (TOP-REAL 2) holds

( x in it iff ( x `1 = p `1 & x `2 >= p `2 ) );

existence for x being Point of (TOP-REAL 2) holds

( x in it iff ( x `1 = p `1 & x `2 >= p `2 ) );

ex b

for x being Point of (TOP-REAL 2) holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

func east_halfline p -> Subset of (TOP-REAL 2) means :Def11: :: TOPREAL1:def 11

for x being Point of (TOP-REAL 2) holds

( x in it iff ( x `1 >= p `1 & x `2 = p `2 ) );

existence for x being Point of (TOP-REAL 2) holds

( x in it iff ( x `1 >= p `1 & x `2 = p `2 ) );

ex b

for x being Point of (TOP-REAL 2) holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

func south_halfline p -> Subset of (TOP-REAL 2) means :Def12: :: TOPREAL1:def 12

for x being Point of (TOP-REAL 2) holds

( x in it iff ( x `1 = p `1 & x `2 <= p `2 ) );

existence for x being Point of (TOP-REAL 2) holds

( x in it iff ( x `1 = p `1 & x `2 <= p `2 ) );

ex b

for x being Point of (TOP-REAL 2) holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

func west_halfline p -> Subset of (TOP-REAL 2) means :Def13: :: TOPREAL1:def 13

for x being Point of (TOP-REAL 2) holds

( x in it iff ( x `1 <= p `1 & x `2 = p `2 ) );

existence for x being Point of (TOP-REAL 2) holds

( x in it iff ( x `1 <= p `1 & x `2 = p `2 ) );

ex b

for x being Point of (TOP-REAL 2) holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def10 defines north_halfline TOPREAL1:def 10 :

for p being Point of (TOP-REAL 2)

for b_{2} being Subset of (TOP-REAL 2) holds

( b_{2} = north_halfline p iff for x being Point of (TOP-REAL 2) holds

( x in b_{2} iff ( x `1 = p `1 & x `2 >= p `2 ) ) );

for p being Point of (TOP-REAL 2)

for b

( b

( x in b

:: deftheorem Def11 defines east_halfline TOPREAL1:def 11 :

for p being Point of (TOP-REAL 2)

for b_{2} being Subset of (TOP-REAL 2) holds

( b_{2} = east_halfline p iff for x being Point of (TOP-REAL 2) holds

( x in b_{2} iff ( x `1 >= p `1 & x `2 = p `2 ) ) );

for p being Point of (TOP-REAL 2)

for b

( b

( x in b

:: deftheorem Def12 defines south_halfline TOPREAL1:def 12 :

for p being Point of (TOP-REAL 2)

for b_{2} being Subset of (TOP-REAL 2) holds

( b_{2} = south_halfline p iff for x being Point of (TOP-REAL 2) holds

( x in b_{2} iff ( x `1 = p `1 & x `2 <= p `2 ) ) );

for p being Point of (TOP-REAL 2)

for b

( b

( x in b

:: deftheorem Def13 defines west_halfline TOPREAL1:def 13 :

for p being Point of (TOP-REAL 2)

for b_{2} being Subset of (TOP-REAL 2) holds

( b_{2} = west_halfline p iff for x being Point of (TOP-REAL 2) holds

( x in b_{2} iff ( x `1 <= p `1 & x `2 = p `2 ) ) );

for p being Point of (TOP-REAL 2)

for b

( b

( x in b

theorem :: TOPREAL1:30

for p being Point of (TOP-REAL 2) holds north_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) }

proof end;

theorem Th31: :: TOPREAL1:31

for p being Point of (TOP-REAL 2) holds north_halfline p = { |[(p `1),r]| where r is Element of REAL : r >= p `2 }

proof end;

theorem :: TOPREAL1:32

for p being Point of (TOP-REAL 2) holds east_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 >= p `1 & q `2 = p `2 ) }

proof end;

theorem Th33: :: TOPREAL1:33

for p being Point of (TOP-REAL 2) holds east_halfline p = { |[r,(p `2)]| where r is Element of REAL : r >= p `1 }

proof end;

theorem :: TOPREAL1:34

for p being Point of (TOP-REAL 2) holds south_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) }

proof end;

theorem Th35: :: TOPREAL1:35

for p being Point of (TOP-REAL 2) holds south_halfline p = { |[(p `1),r]| where r is Element of REAL : r <= p `2 }

proof end;

theorem :: TOPREAL1:36

for p being Point of (TOP-REAL 2) holds west_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 <= p `1 & q `2 = p `2 ) }

proof end;

theorem Th37: :: TOPREAL1:37

for p being Point of (TOP-REAL 2) holds west_halfline p = { |[r,(p `2)]| where r is Element of REAL : r <= p `1 }

proof end;

registration

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

coherence

not north_halfline p is empty

not east_halfline p is empty

not south_halfline p is empty

not west_halfline p is empty

end;
coherence

not north_halfline p is empty

proof end;

coherence not east_halfline p is empty

proof end;

coherence not south_halfline p is empty

proof end;

coherence not west_halfline p is empty

proof end;

:: Moved from JORDAN1C, AK, 23.02.2006

theorem :: TOPREAL1:38

for p being Point of (TOP-REAL 2) holds

( p in west_halfline p & p in east_halfline p & p in north_halfline p & p in south_halfline p )

( p in west_halfline p & p in east_halfline p & p in north_halfline p & p in south_halfline p )

proof end;