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₁ being Element of the carrier of (TOP-REAL 2) holds
( not p in P /\ Q or not b₁ in P /\ Q or LSeg (p,b₁) 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