let a, b, r, s be real number ; :: thesis: closed_inside_of_rectangle a,b,r,s = product (1,2 --> [.a,b.],[.r,s.])
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: product (1,2 --> [.a,b.],[.r,s.]) c= closed_inside_of_rectangle a,b,r,s

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in closed_inside_of_rectangle a,b,r,s or x in product (1,2 --> [.a,b.],[.r,s.]) )
assume x in closed_inside_of_rectangle a,b,r,s ; :: thesis: x in product (1,2 --> [.a,b.],[.r,s.])
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;
|[(p `1 ),(p `2 )]| = 1,2 --> (p `1 ),(p `2 ) by Th25;
then A4: p = 1,2 --> (p `1 ),(p `2 ) by EUCLID:57;
( p `1 in [.a,b.] & p `2 in [.r,s.] ) by A3;
hence x in product (1,2 --> [.a,b.],[.r,s.]) by A2, A4, HILBERT3:11; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in product (1,2 --> [.a,b.],[.r,s.]) or x in closed_inside_of_rectangle a,b,r,s )
assume A5: x in product (1,2 --> [.a,b.],[.r,s.]) ; :: thesis: x in closed_inside_of_rectangle a,b,r,s
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 . 2 in [.r,s.] by A5, A6, Th24;
A9: g . 1 in [.a,b.] by A5, A6, Th24;
then reconsider g1 = g . 1, g2 = g . 2 as Real by A8;
A10: dom (1,2 --> [.a,b.],[.r,s.]) = {1,2} by FUNCT_4:65;
then reconsider g = g as FinSequence by A7, FINSEQ_1:4, FINSEQ_1:def 2;
A11: len g = 2 by A7, A10, FINSEQ_1:4, FINSEQ_1:def 3;
|[g1,g2]| = 1,2 --> g1,g2 by Th25;
then reconsider g = g as Point of (TOP-REAL 2) by A11, FINSEQ_1:61;
A12: ( r <= g `2 & g `2 <= s ) by A8, XXREAL_1:1;
( a <= g `1 & g `1 <= b ) by A9, XXREAL_1:1;
hence x in closed_inside_of_rectangle a,b,r,s by A1, A6, A12; :: thesis: verum