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 ( p in A /\ B & q in A /\ B ) ; :: thesis: p `1 = q `1
then ( p in A & q in A ) by XBOOLE_0:def 4;
hence p `1 = q `1 by SPPOL_1:def 3; :: thesis: verum