let a, b, r, s be Real; 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.]))
XBOOLE_0:def 10 product ((1,2) --> ([.a,b.],[.r,s.])) c= closed_inside_of_rectangle (a,b,r,s)proof
let x be
object ;
TARSKI:def 3 ( 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)
;
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;
verum
end;
let x be object ; TARSKI:def 3 ( 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.]))
; 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; verum