let f be FinSequence of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2) holds

( <*p,q*> is_in_the_area_of f iff ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f ) )

let p, q be Point of (TOP-REAL 2); :: thesis: ( <*p,q*> is_in_the_area_of f iff ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f ) )

thus ( <*p,q*> is_in_the_area_of f implies ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f ) ) :: thesis: ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f implies <*p,q*> is_in_the_area_of f )

dom <*q*> = {1} by FINSEQ_1:2, FINSEQ_1:38;

then A16: 1 in dom <*q*> by TARSKI:def 1;

dom <*p*> = {1} by FINSEQ_1:2, FINSEQ_1:38;

then A17: 1 in dom <*p*> by TARSKI:def 1;

assume A18: <*p*> is_in_the_area_of f ; :: thesis: ( not <*q*> is_in_the_area_of f or <*p,q*> is_in_the_area_of f )

then A19: p `1 <= E-bound (L~ f) by A17, A15;

A20: p `2 <= N-bound (L~ f) by A18, A17, A15;

A21: S-bound (L~ f) <= p `2 by A18, A17, A15;

A22: <*q*> /. 1 = q by FINSEQ_4:16;

assume A23: <*q*> is_in_the_area_of f ; :: thesis: <*p,q*> is_in_the_area_of f

then A24: W-bound (L~ f) <= q `1 by A16, A22;

A25: q `1 <= E-bound (L~ f) by A23, A16, A22;

let i be Nat; :: according to SPRECT_2:def 1 :: thesis: ( not i in dom <*p,q*> or ( W-bound (L~ f) <= (<*p,q*> /. i) `1 & (<*p,q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p,q*> /. i) `2 & (<*p,q*> /. i) `2 <= N-bound (L~ f) ) )

assume i in dom <*p,q*> ; :: thesis: ( W-bound (L~ f) <= (<*p,q*> /. i) `1 & (<*p,q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p,q*> /. i) `2 & (<*p,q*> /. i) `2 <= N-bound (L~ f) )

then i in {1,2} by FINSEQ_1:2, FINSEQ_1:89;

then A26: ( i = 1 or i = 2 ) by TARSKI:def 2;

A27: q `2 <= N-bound (L~ f) by A23, A16, A22;

A28: S-bound (L~ f) <= q `2 by A23, A16, A22;

W-bound (L~ f) <= p `1 by A18, A17, A15;

hence ( W-bound (L~ f) <= (<*p,q*> /. i) `1 & (<*p,q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p,q*> /. i) `2 & (<*p,q*> /. i) `2 <= N-bound (L~ f) ) by A19, A21, A20, A24, A25, A28, A27, A26, FINSEQ_4:17; :: thesis: verum

( <*p,q*> is_in_the_area_of f iff ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f ) )

let p, q be Point of (TOP-REAL 2); :: thesis: ( <*p,q*> is_in_the_area_of f iff ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f ) )

thus ( <*p,q*> is_in_the_area_of f implies ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f ) ) :: thesis: ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f implies <*p,q*> is_in_the_area_of f )

proof

A15:
<*p*> /. 1 = p
by FINSEQ_4:16;
A1:
dom <*p,q*> = {1,2}
by FINSEQ_1:2, FINSEQ_1:89;

then A2: 1 in dom <*p,q*> by TARSKI:def 2;

assume A3: <*p,q*> is_in_the_area_of f ; :: thesis: ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f )

A4: <*p,q*> /. 1 = p by FINSEQ_4:17;

then A5: p `1 <= E-bound (L~ f) by A3, A2;

A6: p `2 <= N-bound (L~ f) by A3, A2, A4;

A7: S-bound (L~ f) <= p `2 by A3, A2, A4;

A8: W-bound (L~ f) <= p `1 by A3, A2, A4;

thus <*p*> is_in_the_area_of f :: thesis: <*q*> is_in_the_area_of f

assume i in dom <*q*> ; :: thesis: ( W-bound (L~ f) <= (<*q*> /. i) `1 & (<*q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*q*> /. i) `2 & (<*q*> /. i) `2 <= N-bound (L~ f) )

then i in {1} by FINSEQ_1:2, FINSEQ_1:38;

then A9: i = 1 by TARSKI:def 1;

A10: <*p,q*> /. 2 = q by FINSEQ_4:17;

A11: 2 in dom <*p,q*> by A1, TARSKI:def 2;

then A12: q `1 <= E-bound (L~ f) by A3, A10;

A13: q `2 <= N-bound (L~ f) by A3, A11, A10;

A14: S-bound (L~ f) <= q `2 by A3, A11, A10;

W-bound (L~ f) <= q `1 by A3, A11, A10;

hence ( W-bound (L~ f) <= (<*q*> /. i) `1 & (<*q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*q*> /. i) `2 & (<*q*> /. i) `2 <= N-bound (L~ f) ) by A12, A14, A13, A9, FINSEQ_4:16; :: thesis: verum

end;then A2: 1 in dom <*p,q*> by TARSKI:def 2;

assume A3: <*p,q*> is_in_the_area_of f ; :: thesis: ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f )

A4: <*p,q*> /. 1 = p by FINSEQ_4:17;

then A5: p `1 <= E-bound (L~ f) by A3, A2;

A6: p `2 <= N-bound (L~ f) by A3, A2, A4;

A7: S-bound (L~ f) <= p `2 by A3, A2, A4;

A8: W-bound (L~ f) <= p `1 by A3, A2, A4;

thus <*p*> is_in_the_area_of f :: thesis: <*q*> is_in_the_area_of f

proof

let i be Nat; :: according to SPRECT_2:def 1 :: thesis: ( not i in dom <*q*> or ( W-bound (L~ f) <= (<*q*> /. i) `1 & (<*q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*q*> /. i) `2 & (<*q*> /. i) `2 <= N-bound (L~ f) ) )
let i be Nat; :: according to SPRECT_2:def 1 :: thesis: ( not i in dom <*p*> or ( W-bound (L~ f) <= (<*p*> /. i) `1 & (<*p*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p*> /. i) `2 & (<*p*> /. i) `2 <= N-bound (L~ f) ) )

assume i in dom <*p*> ; :: thesis: ( W-bound (L~ f) <= (<*p*> /. i) `1 & (<*p*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p*> /. i) `2 & (<*p*> /. i) `2 <= N-bound (L~ f) )

then i in {1} by FINSEQ_1:2, FINSEQ_1:38;

then i = 1 by TARSKI:def 1;

hence ( W-bound (L~ f) <= (<*p*> /. i) `1 & (<*p*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p*> /. i) `2 & (<*p*> /. i) `2 <= N-bound (L~ f) ) by A8, A5, A7, A6, FINSEQ_4:16; :: thesis: verum

end;assume i in dom <*p*> ; :: thesis: ( W-bound (L~ f) <= (<*p*> /. i) `1 & (<*p*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p*> /. i) `2 & (<*p*> /. i) `2 <= N-bound (L~ f) )

then i in {1} by FINSEQ_1:2, FINSEQ_1:38;

then i = 1 by TARSKI:def 1;

hence ( W-bound (L~ f) <= (<*p*> /. i) `1 & (<*p*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p*> /. i) `2 & (<*p*> /. i) `2 <= N-bound (L~ f) ) by A8, A5, A7, A6, FINSEQ_4:16; :: thesis: verum

assume i in dom <*q*> ; :: thesis: ( W-bound (L~ f) <= (<*q*> /. i) `1 & (<*q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*q*> /. i) `2 & (<*q*> /. i) `2 <= N-bound (L~ f) )

then i in {1} by FINSEQ_1:2, FINSEQ_1:38;

then A9: i = 1 by TARSKI:def 1;

A10: <*p,q*> /. 2 = q by FINSEQ_4:17;

A11: 2 in dom <*p,q*> by A1, TARSKI:def 2;

then A12: q `1 <= E-bound (L~ f) by A3, A10;

A13: q `2 <= N-bound (L~ f) by A3, A11, A10;

A14: S-bound (L~ f) <= q `2 by A3, A11, A10;

W-bound (L~ f) <= q `1 by A3, A11, A10;

hence ( W-bound (L~ f) <= (<*q*> /. i) `1 & (<*q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*q*> /. i) `2 & (<*q*> /. i) `2 <= N-bound (L~ f) ) by A12, A14, A13, A9, FINSEQ_4:16; :: thesis: verum

dom <*q*> = {1} by FINSEQ_1:2, FINSEQ_1:38;

then A16: 1 in dom <*q*> by TARSKI:def 1;

dom <*p*> = {1} by FINSEQ_1:2, FINSEQ_1:38;

then A17: 1 in dom <*p*> by TARSKI:def 1;

assume A18: <*p*> is_in_the_area_of f ; :: thesis: ( not <*q*> is_in_the_area_of f or <*p,q*> is_in_the_area_of f )

then A19: p `1 <= E-bound (L~ f) by A17, A15;

A20: p `2 <= N-bound (L~ f) by A18, A17, A15;

A21: S-bound (L~ f) <= p `2 by A18, A17, A15;

A22: <*q*> /. 1 = q by FINSEQ_4:16;

assume A23: <*q*> is_in_the_area_of f ; :: thesis: <*p,q*> is_in_the_area_of f

then A24: W-bound (L~ f) <= q `1 by A16, A22;

A25: q `1 <= E-bound (L~ f) by A23, A16, A22;

let i be Nat; :: according to SPRECT_2:def 1 :: thesis: ( not i in dom <*p,q*> or ( W-bound (L~ f) <= (<*p,q*> /. i) `1 & (<*p,q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p,q*> /. i) `2 & (<*p,q*> /. i) `2 <= N-bound (L~ f) ) )

assume i in dom <*p,q*> ; :: thesis: ( W-bound (L~ f) <= (<*p,q*> /. i) `1 & (<*p,q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p,q*> /. i) `2 & (<*p,q*> /. i) `2 <= N-bound (L~ f) )

then i in {1,2} by FINSEQ_1:2, FINSEQ_1:89;

then A26: ( i = 1 or i = 2 ) by TARSKI:def 2;

A27: q `2 <= N-bound (L~ f) by A23, A16, A22;

A28: S-bound (L~ f) <= q `2 by A23, A16, A22;

W-bound (L~ f) <= p `1 by A18, A17, A15;

hence ( W-bound (L~ f) <= (<*p,q*> /. i) `1 & (<*p,q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p,q*> /. i) `2 & (<*p,q*> /. i) `2 <= N-bound (L~ f) ) by A19, A21, A20, A24, A25, A28, A27, A26, FINSEQ_4:17; :: thesis: verum