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 A1: ( p in P /\ Q & q in P /\ Q ) ; :: thesis: LSeg p,q c= P /\ Q
then ( p in P & q in P ) by XBOOLE_0:def 4;
then A2: LSeg p,q c= P by JORDAN1:def 1;
( p in Q & q in Q ) by A1, XBOOLE_0:def 4;
then LSeg p,q c= Q by JORDAN1:def 1;
hence LSeg p,q c= P /\ Q by A2, XBOOLE_1:19; :: thesis: verum