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