let a, b, r, s be real number ; :: thesis:
set A = [.a,b.];
set B = [.r,s.];
set f = 1,2 --> [.a,b.],[.r,s.];
set R = closed_inside_of_rectangle a,b,r,s;
A1: closed_inside_of_rectangle a,b,r,s = { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & r <= p `2 & p `2 <= s ) } by JGRAPH_6:def 2;
thus closed_inside_of_rectangle a,b,r,s c= product (1,2 --> [.a,b.],[.r,s.]) :: according to XBOOLE_0:def 10 :: thesis:

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in closed_inside_of_rectangle a,b,r,s ; :: thesis:
then consider p being Point of (TOP-REAL 2) such that
A2: x = p and
A3: ( a <= p `1 & p `1 <= b & r <= p `2 & p `2 <= s ) by A1;
A4: ( p `1 in [.a,b.] & p `2 in [.r,s.] ) by A3;
|[(p `1 ),(p `2 )]| = 1,2 --> (p `1 ),(p `2 ) by Th25;
then p = 1,2 --> (p `1 ),(p `2 ) by EUCLID:57;
hence x in product (1,2 --> [.a,b.],[.r,s.]) by A2, A4, HILBERT3:11; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A5: x in product (1,2 --> [.a,b.],[.r,s.]) ; :: thesis:
then consider g being Function such that
A6: x = g and
A7: dom g = dom (1,2 --> [.a,b.],[.r,s.]) and
for y being set st y in dom (1,2 --> [.a,b.],[.r,s.]) holds
g . y in (1,2 --> [.a,b.],[.r,s.]) . y by CARD_3:def 5;
A8: ( g . 1 in [.a,b.] & g . 2 in [.r,s.] ) by A5, A6, Th24;
A9: dom (1,2 --> [.a,b.],[.r,s.]) = {1,2} by FUNCT_4:65;
reconsider g1 = g . 1, g2 = g . 2 as Real by A8;
A10: |[g1,g2]| = 1,2 --> g1,g2 by Th25;
reconsider g = g as FinSequence by A7, A9, FINSEQ_1:4, FINSEQ_1:def 2;
len g = 2 by A7, A9, FINSEQ_1:4, FINSEQ_1:def 3;
then reconsider g = g as Point of (TOP-REAL 2) by A10, FINSEQ_1:61;
( a <= g `1 & g `1 <= b & r <= g `2 & g `2 <= s ) by A8, XXREAL_1:1;
hence x in closed_inside_of_rectangle a,b,r,s by A1, A6; :: thesis: