let B be Subset of (TOP-REAL 2); :: thesis: for A being horizontal Subset of (TOP-REAL 2) holds A /\ B is horizontal
let A be horizontal Subset of (TOP-REAL 2); :: thesis: A /\ B is horizontal
let p, q be Point of (TOP-REAL 2); :: according to SPPOL_1:def 2 :: thesis: ( not p in A /\ B or not q in A /\ B or p `2 = q `2 )
assume ( p in A /\ B & q in A /\ B ) ; :: thesis: p `2 = q `2
then ( p in A & q in A ) by XBOOLE_0:def 4;
hence p `2 = q `2 by SPPOL_1:def 2; :: thesis: verum