:: TOPREALA semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

set R = the carrier of R^1 ;

Lm1: the carrier of [:R^1 ,R^1 :] = [:the carrier of R^1 ,the carrier of R^1 :]
by BORSUK_1:def 5;

reconsider p1 = 1 as real positive number ;

theorem :: TOPREALA:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Integer
for r being real number holds frac (r + i) = frac r
proof end;

theorem Th2: :: TOPREALA:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, a being real number st r <= a & a < [\r/] + 1 holds
[\a/] = [\r/]
proof end;

theorem Th3: :: TOPREALA:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, a being real number st r <= a & a < [\r/] + 1 holds
frac r <= frac a
proof end;

theorem :: TOPREALA:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, a being real number st r < a & a < [\r/] + 1 holds
frac r < frac a
proof end;

theorem Th5: :: TOPREALA:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, r being real number st a >= [\r/] + 1 & a <= r + 1 holds
[\a/] = [\r/] + 1
proof end;

theorem Th6: :: TOPREALA:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, r being real number st a >= [\r/] + 1 & a < r + 1 holds
frac a < frac r
proof end;

theorem :: TOPREALA:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, a, b being real number st r <= a & a < r + 1 & r <= b & b < r + 1 & frac a = frac b holds
a = b
proof end;

registration
let r be real number ;
let s be real positive number ;
cluster ].r,(r + s).[ -> non empty ;
coherence
not ].r,(r + s).[ is empty
proof end;
cluster [.r,(r + s).[ -> non empty ;
coherence
not [.r,(r + s).[ is empty
proof end;
cluster ].r,(r + s).] -> non empty ;
coherence
not ].r,(r + s).] is empty
proof end;
cluster [.r,(r + s).] -> non empty ;
coherence
not [.r,(r + s).] is empty
proof end;
cluster ].(r - s),r.[ -> non empty ;
coherence
not ].(r - s),r.[ is empty
proof end;
cluster [.(r - s),r.[ -> non empty ;
coherence
not [.(r - s),r.[ is empty
proof end;
cluster ].(r - s),r.] -> non empty ;
coherence
not ].(r - s),r.] is empty
proof end;
cluster [.(r - s),r.] -> non empty ;
coherence
not [.(r - s),r.] is empty
proof end;
end;

registration
let r be real non positive number ;
let s be real positive number ;
cluster ].r,s.[ -> non empty ;
coherence
not ].r,s.[ is empty
proof end;
cluster [.r,s.[ -> non empty ;
coherence
not [.r,s.[ is empty
by RCOMP_2:3;
cluster ].r,s.] -> non empty ;
coherence
not ].r,s.] is empty
by RCOMP_2:4;
cluster [.r,s.] -> non empty ;
coherence
not [.r,s.] is empty
by RCOMP_1:48;
end;

registration
let r be real negative number ;
let s be real non negative number ;
cluster ].r,s.[ -> non empty ;
coherence
not ].r,s.[ is empty
proof end;
cluster [.r,s.[ -> non empty ;
coherence
not [.r,s.[ is empty
by RCOMP_2:3;
cluster ].r,s.] -> non empty ;
coherence
not ].r,s.] is empty
by RCOMP_2:4;
cluster [.r,s.] -> non empty ;
coherence
not [.r,s.] is empty
by RCOMP_1:48;
end;

theorem :: TOPREALA:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, a, b, s being real number st r <= a & b < s holds
[.a,b.] c= [.r,s.[
proof end;

theorem :: TOPREALA:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, a, b, s being real number st r < a & b <= s holds
[.a,b.] c= ].r,s.]
proof end;

theorem :: TOPREALA:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, a, b, s being real number st r < a & b < s holds
[.a,b.] c= ].r,s.[
proof end;

theorem Th11: :: TOPREALA:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, a, b, s being real number st r <= a & b <= s holds
[.a,b.[ c= [.r,s.]
proof end;

theorem :: TOPREALA:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, a, b, s being real number st r <= a & b <= s holds
[.a,b.[ c= [.r,s.[
proof end;

theorem :: TOPREALA:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, a, b, s being real number st r < a & b <= s holds
[.a,b.[ c= ].r,s.]
proof end;

theorem Th14: :: TOPREALA:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, a, b, s being real number st r < a & b <= s holds
[.a,b.[ c= ].r,s.[
proof end;

theorem Th15: :: TOPREALA:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, a, b, s being real number st r <= a & b <= s holds
].a,b.] c= [.r,s.]
proof end;

theorem :: TOPREALA:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, a, b, s being real number st r <= a & b < s holds
].a,b.] c= [.r,s.[
proof end;

theorem :: TOPREALA:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, a, b, s being real number st r <= a & b <= s holds
].a,b.] c= ].r,s.]
proof end;

theorem Th18: :: TOPREALA:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, a, b, s being real number st r <= a & b < s holds
].a,b.] c= ].r,s.[
proof end;

theorem Th19: :: TOPREALA:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, a, b, s being real number st r <= a & b <= s holds
].a,b.[ c= [.r,s.]
proof end;

theorem :: TOPREALA:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, a, b, s being real number st r <= a & b <= s holds
].a,b.[ c= [.r,s.[
proof end;

theorem :: TOPREALA:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, a, b, s being real number st r <= a & b <= s holds
].a,b.[ c= ].r,s.]
proof end;

theorem :: TOPREALA:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function
for x, X being set st x in dom f & f . x in f .: X & f is one-to-one holds
x in X
proof end;

theorem :: TOPREALA:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence
for i being natural number holds
( not i + 1 in dom f or i in dom f or i = 0 )
proof end;

theorem Th24: :: TOPREALA:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, X, Y being set
for f being Function st x <> y & f in product (x,y --> X,Y) holds
( f . x in X & f . y in Y )
proof end;

theorem Th25: :: TOPREALA:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being set holds <*a,b*> = 1,2 --> a,b
proof end;

registration
cluster non empty strict constituted-FinSeqs TopStruct ;
existence
ex b1 being TopSpace st
( b1 is constituted-FinSeqs & not b1 is empty & b1 is strict )
proof end;
end;

registration
let T be constituted-FinSeqs TopSpace;
cluster -> constituted-FinSeqs SubSpace of T;
coherence
for b1 being SubSpace of T holds b1 is constituted-FinSeqs
proof end;
end;

theorem Th26: :: TOPREALA:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for Z being non empty SubSpace of T
for t being Point of T
for z being Point of Z
for N being open a_neighborhood of t
for M being Subset of Z st t = z & M = N /\ ([#] Z) holds
M is open a_neighborhood of z
proof end;

registration
cluster empty -> discrete anti-discrete TopStruct ;
coherence
for b1 being TopSpace st b1 is empty holds
( b1 is discrete & b1 is anti-discrete )
proof end;
end;

registration
let X be discrete TopSpace;
let Y be TopSpace;
cluster -> continuous Relation of the carrier of X,the carrier of Y;
coherence
for b1 being Function of X,Y holds b1 is continuous
by TEX_2:68;
end;

theorem Th27: :: TOPREALA:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being TopSpace
for Y being TopStruct
for f being Function of X,Y st f is empty holds
f is continuous
proof end;

registration
let X be TopSpace;
let Y be TopStruct ;
cluster empty -> continuous Relation of the carrier of X,the carrier of Y;
coherence
for b1 being Function of X,Y st b1 is empty holds
b1 is continuous
by Th27;
end;

theorem :: TOPREALA:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being TopStruct
for Y being non empty TopStruct
for Z being non empty SubSpace of Y
for f being Function of X,Z holds f is Function of X,Y
proof end;

theorem :: TOPREALA:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty TopSpace
for X being Subset of S
for Y being Subset of T
for f being continuous Function of S,T
for g being Function of (S | X),(T | Y) st g = f | X holds
g is continuous
proof end;

theorem :: TOPREALA:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty TopSpace
for Z being non empty SubSpace of T
for f being Function of S,T
for g being Function of S,Z st f = g & f is open holds
g is open
proof end;

theorem :: TOPREALA:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty TopSpace
for S1 being Subset of S
for T1 being Subset of T
for f being Function of S,T
for g being Function of (S | S1),(T | T1) st g = f | S1 & g is onto & f is open & f is one-to-one holds
g is open
proof end;

theorem :: TOPREALA:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y, Z being non empty TopSpace
for f being Function of X,Y
for g being Function of Y,Z st f is open & g is open holds
g * f is open
proof end;

theorem :: TOPREALA:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being TopSpace
for Z being open SubSpace of Y
for f being Function of X,Y
for g being Function of X,Z st f = g & g is open holds
f is open
proof end;

theorem Th34: :: TOPREALA:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty TopSpace
for f being Function of S,T st f is one-to-one & f is onto holds
( f is continuous iff f " is open )
proof end;

theorem :: TOPREALA:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty TopSpace
for f being Function of S,T st f is one-to-one & f is onto holds
( f is open iff f " is continuous )
proof end;

theorem :: TOPREALA:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being TopSpace
for T being non empty TopSpace holds
( S,T are_homeomorphic iff TopStruct(# the carrier of S,the topology of S #), TopStruct(# the carrier of T,the topology of T #) are_homeomorphic )
proof end;

theorem :: TOPREALA:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty TopSpace
for f being Function of S,T st f is one-to-one & f is onto & f is continuous & f is open holds
f is_homeomorphism
proof end;

theorem :: TOPREALA:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number
for f being PartFunc of REAL , REAL st f = REAL --> r holds
f is_continuous_on REAL
proof end;

theorem :: TOPREALA:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, f1, f2 being PartFunc of REAL , REAL st dom f = (dom f1) \/ (dom f2) & dom f1 is open & dom f2 is open & f1 is_continuous_on dom f1 & f2 is_continuous_on dom f2 & ( for z being set st z in dom f1 holds
f . z = f1 . z ) & ( for z being set st z in dom f2 holds
f . z = f2 . z ) holds
f is_continuous_on dom f
proof end;

theorem Th40: :: TOPREALA:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Point of R^1
for N being Subset of REAL
for M being Subset of R^1 st M = N & N is Neighbourhood of x holds
M is a_neighborhood of x
proof end;

theorem Th41: :: TOPREALA:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Point of R^1
for M being a_neighborhood of x ex N being Neighbourhood of x st N c= M
proof end;

theorem Th42: :: TOPREALA:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function of R^1 ,R^1
for g being PartFunc of REAL , REAL
for x being Point of R^1 st f = g & g is_continuous_in x holds
f is_continuous_at x
proof end;

theorem :: TOPREALA:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function of R^1 ,R^1
for g being Function of REAL , REAL st f = g & g is_continuous_on REAL holds
f is continuous
proof end;

theorem :: TOPREALA:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, r, s, b being real number st a <= r & s <= b holds
[.r,s.] is closed Subset of (Closed-Interval-TSpace a,b)
proof end;

theorem :: TOPREALA:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, r, s, b being real number st a <= r & s <= b holds
].r,s.[ is open Subset of (Closed-Interval-TSpace a,b)
proof end;

theorem :: TOPREALA:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, r being real number st a <= b & a <= r holds
].r,b.] is open Subset of (Closed-Interval-TSpace a,b)
proof end;

theorem :: TOPREALA:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, r being real number st a <= b & r <= b holds
[.a,r.[ is open Subset of (Closed-Interval-TSpace a,b)
proof end;

theorem Th48: :: TOPREALA:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, r, s being real number st a <= b & r <= s holds
the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):] = [:[.a,b.],[.r,s.]:]
proof end;

theorem Th49: :: TOPREALA:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number holds |[a,b]| = 1,2 --> a,b
proof end;

theorem :: TOPREALA:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number holds
( |[a,b]| . 1 = a & |[a,b]| . 2 = b )
proof end;

theorem Th51: :: TOPREALA:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, r, s being real number holds closed_inside_of_rectangle a,b,r,s = product (1,2 --> [.a,b.],[.r,s.])
proof end;

theorem Th52: :: TOPREALA:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, r, s being real number st a <= b & r <= s holds
|[a,r]| in closed_inside_of_rectangle a,b,r,s
proof end;

definition
let a, b, c, d be real number ;
func Trectangle a,b,c,d -> SubSpace of TOP-REAL 2 equals :: TOPREALA:def 1
(TOP-REAL 2) | (closed_inside_of_rectangle a,b,c,d);
coherence
(TOP-REAL 2) | (closed_inside_of_rectangle a,b,c,d) is SubSpace of TOP-REAL 2
;
end;

:: deftheorem defines Trectangle TOPREALA:def 1 :
for a, b, c, d being real number holds Trectangle a,b,c,d = (TOP-REAL 2) | (closed_inside_of_rectangle a,b,c,d);

theorem Th53: :: TOPREALA:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, r, s being real number holds the carrier of (Trectangle a,b,r,s) = closed_inside_of_rectangle a,b,r,s by JORDAN1:1;

theorem Th54: :: TOPREALA:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, r, s being real number st a <= b & r <= s holds
not Trectangle a,b,r,s is empty
proof end;

registration
let a, c be real non positive number ;
let b, d be real non negative number ;
cluster Trectangle a,b,c,d -> non empty constituted-FinSeqs ;
coherence
not Trectangle a,b,c,d is empty
by Th54;
end;

definition
func R2Homeomorphism -> Function of [:R^1 ,R^1 :],(TOP-REAL 2) means :Def2: :: TOPREALA:def 2
for x, y being real number holds it . [x,y] = <*x,y*>;
existence
ex b1 being Function of [:R^1 ,R^1 :],(TOP-REAL 2) st
for x, y being real number holds b1 . [x,y] = <*x,y*>
proof end;
uniqueness
for b1, b2 being Function of [:R^1 ,R^1 :],(TOP-REAL 2) st ( for x, y being real number holds b1 . [x,y] = <*x,y*> ) & ( for x, y being real number holds b2 . [x,y] = <*x,y*> ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines R2Homeomorphism TOPREALA:def 2 :
for b1 being Function of [:R^1 ,R^1 :],(TOP-REAL 2) holds
( b1 = R2Homeomorphism iff for x, y being real number holds b1 . [x,y] = <*x,y*> );

theorem Th55: :: TOPREALA:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being Subset of REAL holds R2Homeomorphism .: [:A,B:] = product (1,2 --> A,B)
proof end;

theorem Th56: :: TOPREALA:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
R2Homeomorphism is_homeomorphism
proof end;

theorem Th57: :: TOPREALA:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, r, s being real number st a <= b & r <= s holds
R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):] is Function of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):],(Trectangle a,b,r,s)
proof end;

theorem Th58: :: TOPREALA:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, r, s being real number st a <= b & r <= s holds
for h being Function of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):],(Trectangle a,b,r,s) st h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):] holds
h is_homeomorphism
proof end;

theorem :: TOPREALA:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, r, s being real number st a <= b & r <= s holds
[:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):], Trectangle a,b,r,s are_homeomorphic
proof end;

theorem Th60: :: TOPREALA:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, r, s being real number st a <= b & r <= s holds
for A being Subset of (Closed-Interval-TSpace a,b)
for B being Subset of (Closed-Interval-TSpace r,s) holds product (1,2 --> A,B) is Subset of (Trectangle a,b,r,s)
proof end;

theorem :: TOPREALA:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, r, s being real number st a <= b & r <= s holds
for A being open Subset of (Closed-Interval-TSpace a,b)
for B being open Subset of (Closed-Interval-TSpace r,s) holds product (1,2 --> A,B) is open Subset of (Trectangle a,b,r,s)
proof end;

theorem :: TOPREALA:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, r, s being real number st a <= b & r <= s holds
for A being closed Subset of (Closed-Interval-TSpace a,b)
for B being closed Subset of (Closed-Interval-TSpace r,s) holds product (1,2 --> A,B) is closed Subset of (Trectangle a,b,r,s)
proof end;