let s be real number ; :: thesis: for A being Subset of (TOP-REAL 2) st A c= Vertical_Line s holds
A is vertical
let A be Subset of (TOP-REAL 2); :: thesis: ( A c= Vertical_Line s implies A is vertical )
assume A1: A c= Vertical_Line s ; :: thesis: A is vertical
A2: Vertical_Line s = { p where p is Point of (TOP-REAL 2) : p `1 = s } by JORDAN6:def 6;
for p, q being Point of (TOP-REAL 2) st p in A & q in A holds
p `1 = q `1

proof

let p, q be Point of (TOP-REAL 2); :: thesis: ( p in A & q in A implies p `1 = q `1 )
assume p in A ; :: thesis: ( not q in A or p `1 = q `1 )
then p in Vertical_Line s by A1;
then A3: ex p1 being Point of (TOP-REAL 2) st
( p1 = p & p1 `1 = s ) by A2;
assume q in A ; :: thesis: p `1 = q `1
then q in Vertical_Line s by A1;
then ex p1 being Point of (TOP-REAL 2) st
( p1 = q & p1 `1 = s ) by A2;
hence p `1 = q `1 by A3; :: thesis: verum

end;

hence A is vertical by SPPOL_1:def 3; :: thesis: verum