let B be Subset of (TOP-REAL 2); :: thesis: for A being vertical Subset of (TOP-REAL 2) holds A /\ B is vertical
let A be vertical Subset of (TOP-REAL 2); :: thesis: A /\ B is vertical
let p, q be Point of (TOP-REAL 2); :: according to SPPOL_1:def 3 :: thesis: ( not p in A /\ B or not q in A /\ B or p `1 = q `1 )
assume that
A1: p in A /\ B and
A2: q in A /\ B ; :: thesis: p `1 = q `1
A3: p in A by A1, XBOOLE_0:def 4;
q in A by A2, XBOOLE_0:def 4;
hence p `1 = q `1 by A3, SPPOL_1:def 3; :: thesis: verum