let P, Q be convex Subset of (TOP-REAL 2); P /\ Q is convex
let p be Point of (TOP-REAL 2); JORDAN1:def 1 for b1 being Element of the carrier of (TOP-REAL 2) holds
( not p in P /\ Q or not b1 in P /\ Q or LSeg (p,b1) c= P /\ Q )
let q be Point of (TOP-REAL 2); ( 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
; 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; verum