let p1, p2, p3, p4 be Point of (TOP-REAL 2); :: thesis: for a, b, c, d being real number
for P, Q being Subset of (TOP-REAL 2) st a < b & c < d & p1 `2 = d & p2 `1 = b & p3 `2 = c & p4 `2 = c & a <= p1 `1 & p1 `1 <= b & c <= p2 `2 & p2 `2 <= d & 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 number ; :: thesis: for P, Q being Subset of (TOP-REAL 2) st a < b & c < d & p1 `2 = d & p2 `1 = b & p3 `2 = c & p4 `2 = c & a <= p1 `1 & p1 `1 <= b & c <= p2 `2 & p2 `2 <= d & 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); :: thesis: ( a < b & c < d & p1 `2 = d & p2 `1 = b & p3 `2 = c & p4 `2 = c & a <= p1 `1 & p1 `1 <= b & c <= p2 `2 & p2 `2 <= d & 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 A1: ( a < b & c < d & p1 `2 = d & p2 `1 = b & p3 `2 = c & p4 `2 = c & a <= p1 `1 & p1 `1 <= b & c <= p2 `2 & p2 `2 <= d & 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 ) ; :: thesis: P meets Q
then consider f being Function of I[01] ,(TOP-REAL 2) such that
A2: ( f is continuous & f is one-to-one & rng f = P & f . 0 = p1 & f . 1 = p3 ) by Th2;
consider g being Function of I[01] ,(TOP-REAL 2) such that
A3: ( g is continuous & g is one-to-one & rng g = Q & g . 0 = p2 & g . 1 = p4 ) by A1, Th2;
thus P meets Q by A1, A2, A3, Th124; :: thesis: verum