theorem
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
Real for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `2 = d &
p3 `1 = b &
p4 `1 = b &
c <= p1 `2 &
p1 `2 <= d &
a <= p2 `1 &
p2 `1 <= b &
c <= p4 `2 &
p4 `2 < p3 `2 &
p3 `2 <= d &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle (
a,
b,
c,
d) &
Q c= closed_inside_of_rectangle (
a,
b,
c,
d) holds
P meets Q