let P, Q be convex Subset of (TOP-REAL 2); :: thesis: P /\ Q is convex

let p be Point of (TOP-REAL 2); :: according to JORDAN1:def 1 :: thesis: for b_{1} being Element of the carrier of (TOP-REAL 2) holds

( not p in P /\ Q or not b_{1} in P /\ Q or LSeg (p,b_{1}) c= P /\ Q )

let q be Point of (TOP-REAL 2); :: thesis: ( not p in P /\ Q or not q in P /\ Q or LSeg (p,q) c= P /\ Q )

assume that

A1: p in P /\ Q and

A2: q in P /\ Q ; :: thesis: LSeg (p,q) c= P /\ Q

A3: p in P by A1, XBOOLE_0:def 4;

q in P by A2, XBOOLE_0:def 4;

then A4: LSeg (p,q) c= P by A3, JORDAN1:def 1;

A5: p in Q by A1, XBOOLE_0:def 4;

q in Q by A2, XBOOLE_0:def 4;

then LSeg (p,q) c= Q by A5, JORDAN1:def 1;

hence LSeg (p,q) c= P /\ Q by A4, XBOOLE_1:19; :: thesis: verum

let p be Point of (TOP-REAL 2); :: according to JORDAN1:def 1 :: thesis: for b

( not p in P /\ Q or not b

let q be Point of (TOP-REAL 2); :: thesis: ( not p in P /\ Q or not q in P /\ Q or LSeg (p,q) c= P /\ Q )

assume that

A1: p in P /\ Q and

A2: q in P /\ Q ; :: thesis: LSeg (p,q) c= P /\ Q

A3: p in P by A1, XBOOLE_0:def 4;

q in P by A2, XBOOLE_0:def 4;

then A4: LSeg (p,q) c= P by A3, JORDAN1:def 1;

A5: p in Q by A1, XBOOLE_0:def 4;

q in Q by A2, XBOOLE_0:def 4;

then LSeg (p,q) c= Q by A5, JORDAN1:def 1;

hence LSeg (p,q) c= P /\ Q by A4, XBOOLE_1:19; :: thesis: verum