let f be FinSequence of (); :: thesis: for p, q being Point of () 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 (); :: 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
A1: dom <*p,q*> = {1,2} by ;
then A2: 1 in dom <*p,q*> by TARSKI:def 2;
assume A3: <*p,q*> is_in_the_area_of f ; :: thesis:
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:
proof
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 ;
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 ; :: thesis: verum
end;
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) ) )
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 ;
then A9: i = 1 by TARSKI:def 1;
A10: <*p,q*> /. 2 = q by FINSEQ_4:17;
A11: 2 in dom <*p,q*> by ;
then A12: q `1 <= E-bound (L~ f) by ;
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 ; :: thesis: verum
end;
A15: <*p*> /. 1 = p by FINSEQ_4:16;
dom <*q*> = {1} by ;
then A16: 1 in dom <*q*> by TARSKI:def 1;
dom <*p*> = {1} by ;
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 ;
A20: p `2 <= N-bound (L~ f) by ;
A21: S-bound (L~ f) <= p `2 by ;
A22: <*q*> /. 1 = q by FINSEQ_4:16;
assume A23: <*q*> is_in_the_area_of f ; :: thesis:
then A24: W-bound (L~ f) <= q `1 by ;
A25: q `1 <= E-bound (L~ f) by ;
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 ;
then A26: ( i = 1 or i = 2 ) by TARSKI:def 2;
A27: q `2 <= N-bound (L~ f) by ;
A28: S-bound (L~ f) <= q `2 by ;
W-bound (L~ f) <= p `1 by ;
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 ; :: thesis: verum