let A, B be Subset of (TOP-REAL 2); :: thesis: ( A c= B & B is horizontal implies A is horizontal )
assume that
A1: A c= B and
A2: B is horizontal ; :: thesis: A is horizontal
let p be Point of (TOP-REAL 2); :: according to SPPOL_1:def 2 :: thesis: for b₁ being Element of the carrier of (TOP-REAL 2) holds
( not p in A or not b₁ in A or p `2 = b<sub>1</sub> `2 )
let q be Point of (TOP-REAL 2); :: thesis: ( not p in A or not q in A or p `2 = q `2 )
assume that
A3: p in A and
A4: q in A ; :: thesis: p `2 = q `2
thus p `2 = q `2 by A1, A2, A3, A4, SPPOL_1:def 2; :: thesis: verum