let p1, p2, p3, p4 be 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 `2 = c & p4 `2 = c & c <= p1 `2 & p1 `2 <= d & a <= p2 `1 & p2 `1 <= b & a < p4 `1 & p4 `1 < p3 `1 & p3 `1 <= b & 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
let a, b, c, d be Real; for P, Q being Subset of (TOP-REAL 2) st a < b & c < d & p1 `1 = a & p2 `2 = d & p3 `2 = c & p4 `2 = c & c <= p1 `2 & p1 `2 <= d & a <= p2 `1 & p2 `1 <= b & a < p4 `1 & p4 `1 < p3 `1 & p3 `1 <= b & 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
let P, Q be Subset of (TOP-REAL 2); ( a < b & c < d & p1 `1 = a & p2 `2 = d & p3 `2 = c & p4 `2 = c & c <= p1 `2 & p1 `2 <= d & a <= p2 `1 & p2 `1 <= b & a < p4 `1 & p4 `1 < p3 `1 & p3 `1 <= b & 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) implies P meets Q )
assume that
A1:
a < b
and
A2:
c < d
and
A3:
p1 `1 = a
and
A4:
p2 `2 = d
and
A5:
p3 `2 = c
and
A6:
p4 `2 = c
and
A7:
c <= p1 `2
and
A8:
p1 `2 <= d
and
A9:
a <= p2 `1
and
A10:
p2 `1 <= b
and
A11:
a < p4 `1
and
A12:
p4 `1 < p3 `1
and
A13:
p3 `1 <= b
and
A14:
P is_an_arc_of p1,p3
and
A15:
Q is_an_arc_of p2,p4
and
A16:
P c= closed_inside_of_rectangle (a,b,c,d)
and
A17:
Q c= closed_inside_of_rectangle (a,b,c,d)
; P meets Q
A18:
ex g being Function of I[01],(TOP-REAL 2) st
( g is continuous & g is one-to-one & rng g = Q & g . 0 = p2 & g . 1 = p4 )
by A15, Th2;
ex f being Function of I[01],(TOP-REAL 2) st
( f is continuous & f is one-to-one & rng f = P & f . 0 = p1 & f . 1 = p3 )
by A14, Th2;
hence
P meets Q
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A16, A17, A18, Th98; verum