let i, k be Nat; :: thesis: for C being non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge (C,i)) & (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) & p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) holds

ex j being Nat st

( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) )

let C be non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge (C,i)) & (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) & p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) holds

ex j being Nat st

( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) )

let p be Point of (TOP-REAL 2); :: thesis: ( p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge (C,i)) & (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) & p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) implies ex j being Nat st

( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) ) )

assume that

A1: p `1 = ((W-bound C) + (E-bound C)) / 2 and

A2: i > 0 and

A3: 1 <= k and

A4: k <= width (Gauge (C,i)) and

A5: (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) and

A6: p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) ; :: thesis: ex j being Nat st

( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) )

set f = Lower_Seq (C,i);

set G = Gauge (C,i);

A7: Center (Gauge (C,i)) <= len (Gauge (C,i)) by JORDAN1B:13;

4 <= len (Gauge (C,i)) by JORDAN8:10;

then A8: 1 <= len (Gauge (C,i)) by XXREAL_0:2;

4 <= len (Gauge (C,1)) by JORDAN8:10;

then 1 <= len (Gauge (C,1)) by XXREAL_0:2;

then A9: ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `1 by A2, A8, JORDAN1A:36;

A10: ( 1 <= Center (Gauge (C,1)) & Center (Gauge (C,1)) <= len (Gauge (C,1)) ) by JORDAN1B:11, JORDAN1B:13;

A11: 1 <= Center (Gauge (C,i)) by JORDAN1B:11;

then A12: ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `1 by A3, A4, A7, GOBOARD5:2;

0 + 1 <= i by A2, NAT_1:13;

then A13: ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 by A11, A7, A10, JORDAN1A:43;

A14: (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) c= (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i)))

((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2 by A3, A4, A11, A7, JORDAN1A:19;

then (Gauge (C,i)) * ((Center (Gauge (C,i))),1) in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) by A9, A12, A13, GOBOARD7:7;

then LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) c= LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) by A20, TOPREAL1:6;

then (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) c= (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) by XBOOLE_1:27;

then (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) = (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) by A14, XBOOLE_0:def 10;

then A21: upper_bound (proj2 .: ((LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))))) = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) by A2, JORDAN1G:56;

A22: ( Lower_Seq (C,i) is_sequence_on Gauge (C,i) & Upper_Arc (L~ (Cage (C,i))) c= L~ (Cage (C,i)) ) by JORDAN1F:12, JORDAN6:61;

len (Gauge (C,i)) >= 4 by JORDAN8:10;

then width (Gauge (C,i)) >= 4 by JORDAN8:def 1;

then 1 <= width (Gauge (C,i)) by XXREAL_0:2;

then A23: [(Center (Gauge (C,i))),1] in Indices (Gauge (C,i)) by A11, A7, MATRIX_0:30;

[(Center (Gauge (C,i))),k] in Indices (Gauge (C,i)) by A3, A4, A11, A7, MATRIX_0:30;

then consider n being Nat such that

A24: 1 <= n and

A25: n <= k and

A26: ((Gauge (C,i)) * ((Center (Gauge (C,i))),n)) `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))))) by A3, A4, A5, A11, A7, A23, A22, JORDAN1F:2, JORDAN1G:46;

take n ; :: thesis: ( 1 <= n & n <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n) )

thus 1 <= n by A24; :: thesis: ( n <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n) )

thus n <= width (Gauge (C,i)) by A4, A25, XXREAL_0:2; :: thesis: p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n)

then p `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),n)) `1 by A1, A2, A24, JORDAN1G:35;

hence p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n) by A6, A26, A21, TOPREAL3:6; :: thesis: verum

for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge (C,i)) & (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) & p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) holds

ex j being Nat st

( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) )

let C be non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge (C,i)) & (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) & p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) holds

ex j being Nat st

( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) )

let p be Point of (TOP-REAL 2); :: thesis: ( p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge (C,i)) & (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) & p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) implies ex j being Nat st

( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) ) )

assume that

A1: p `1 = ((W-bound C) + (E-bound C)) / 2 and

A2: i > 0 and

A3: 1 <= k and

A4: k <= width (Gauge (C,i)) and

A5: (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) and

A6: p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) ; :: thesis: ex j being Nat st

( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) )

set f = Lower_Seq (C,i);

set G = Gauge (C,i);

A7: Center (Gauge (C,i)) <= len (Gauge (C,i)) by JORDAN1B:13;

4 <= len (Gauge (C,i)) by JORDAN8:10;

then A8: 1 <= len (Gauge (C,i)) by XXREAL_0:2;

4 <= len (Gauge (C,1)) by JORDAN8:10;

then 1 <= len (Gauge (C,1)) by XXREAL_0:2;

then A9: ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `1 by A2, A8, JORDAN1A:36;

A10: ( 1 <= Center (Gauge (C,1)) & Center (Gauge (C,1)) <= len (Gauge (C,1)) ) by JORDAN1B:11, JORDAN1B:13;

A11: 1 <= Center (Gauge (C,i)) by JORDAN1B:11;

then A12: ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `1 by A3, A4, A7, GOBOARD5:2;

0 + 1 <= i by A2, NAT_1:13;

then A13: ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 by A11, A7, A10, JORDAN1A:43;

A14: (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) c= (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i)))

proof

A20:
(Gauge (C,i)) * ((Center (Gauge (C,i))),k) in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))
by RLTOPSP1:68;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) or a in (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) )

assume A15: a in (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) ; :: thesis: a in (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i)))

then reconsider q = a as Point of (TOP-REAL 2) ;

A16: a in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) by A15, XBOOLE_0:def 4;

A17: a in L~ (Lower_Seq (C,i)) by A15, XBOOLE_0:def 4;

then q in (L~ (Lower_Seq (C,i))) \/ (L~ (Upper_Seq (C,i))) by XBOOLE_0:def 3;

then q in L~ (Cage (C,i)) by JORDAN1E:13;

then S-bound (L~ (Cage (C,i))) <= q `2 by PSCOMP_1:24;

then A18: ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 <= q `2 by A7, JORDAN1A:72, JORDAN1B:11;

((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2 by A3, A4, A11, A7, JORDAN1A:19;

then ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2 by A13, XXREAL_0:2;

then A19: q `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2 by A16, TOPREAL1:4;

q `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `1 by A9, A12, A16, GOBOARD7:5;

then q in LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) by A12, A19, A18, GOBOARD7:7;

hence a in (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) by A17, XBOOLE_0:def 4; :: thesis: verum

end;assume A15: a in (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) ; :: thesis: a in (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i)))

then reconsider q = a as Point of (TOP-REAL 2) ;

A16: a in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) by A15, XBOOLE_0:def 4;

A17: a in L~ (Lower_Seq (C,i)) by A15, XBOOLE_0:def 4;

then q in (L~ (Lower_Seq (C,i))) \/ (L~ (Upper_Seq (C,i))) by XBOOLE_0:def 3;

then q in L~ (Cage (C,i)) by JORDAN1E:13;

then S-bound (L~ (Cage (C,i))) <= q `2 by PSCOMP_1:24;

then A18: ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 <= q `2 by A7, JORDAN1A:72, JORDAN1B:11;

((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2 by A3, A4, A11, A7, JORDAN1A:19;

then ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2 by A13, XXREAL_0:2;

then A19: q `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2 by A16, TOPREAL1:4;

q `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `1 by A9, A12, A16, GOBOARD7:5;

then q in LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) by A12, A19, A18, GOBOARD7:7;

hence a in (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) by A17, XBOOLE_0:def 4; :: thesis: verum

((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2 by A3, A4, A11, A7, JORDAN1A:19;

then (Gauge (C,i)) * ((Center (Gauge (C,i))),1) in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) by A9, A12, A13, GOBOARD7:7;

then LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) c= LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) by A20, TOPREAL1:6;

then (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) c= (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) by XBOOLE_1:27;

then (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) = (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) by A14, XBOOLE_0:def 10;

then A21: upper_bound (proj2 .: ((LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))))) = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) by A2, JORDAN1G:56;

A22: ( Lower_Seq (C,i) is_sequence_on Gauge (C,i) & Upper_Arc (L~ (Cage (C,i))) c= L~ (Cage (C,i)) ) by JORDAN1F:12, JORDAN6:61;

len (Gauge (C,i)) >= 4 by JORDAN8:10;

then width (Gauge (C,i)) >= 4 by JORDAN8:def 1;

then 1 <= width (Gauge (C,i)) by XXREAL_0:2;

then A23: [(Center (Gauge (C,i))),1] in Indices (Gauge (C,i)) by A11, A7, MATRIX_0:30;

[(Center (Gauge (C,i))),k] in Indices (Gauge (C,i)) by A3, A4, A11, A7, MATRIX_0:30;

then consider n being Nat such that

A24: 1 <= n and

A25: n <= k and

A26: ((Gauge (C,i)) * ((Center (Gauge (C,i))),n)) `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))))) by A3, A4, A5, A11, A7, A23, A22, JORDAN1F:2, JORDAN1G:46;

take n ; :: thesis: ( 1 <= n & n <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n) )

thus 1 <= n by A24; :: thesis: ( n <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n) )

thus n <= width (Gauge (C,i)) by A4, A25, XXREAL_0:2; :: thesis: p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n)

then p `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),n)) `1 by A1, A2, A24, JORDAN1G:35;

hence p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n) by A6, A26, A21, TOPREAL3:6; :: thesis: verum