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 that
A1: p in A /\ B and
A2: q in A /\ B ; :: thesis: p `2 = q `2
A3: p in A by A1, XBOOLE_0:def 4;
q in A by A2, XBOOLE_0:def 4;
hence p `2 = q `2 by A3, SPPOL_1:def 2; :: thesis: verum