let a, b, r, s be Real; :: 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 object ; :: 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 Th4;
then A4: p = (1,2) --> ((p `1),(p `2)) by EUCLID:53;
( 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 object ; :: 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 object 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, Th3;
A9: g . 1 in [.a,b.] by A5, A6, Th3;
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:62;
then reconsider g = g as FinSequence by A7, FINSEQ_1:2, FINSEQ_1:def 2;
A11: len g = 2 by A7, A10, FINSEQ_1:2, FINSEQ_1:def 3;
|[g1,g2]| = (1,2) --> (g1,g2) by Th4;
then reconsider g = g as Point of (TOP-REAL 2) by A11, FINSEQ_1:44;
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