let p, q be Point of (TOP-REAL 2); :: thesis: for s being Real st p in Vertical_Line s & q in Vertical_Line s holds
LSeg (p,q) c= Vertical_Line s
let s be Real; :: thesis: ( p in Vertical_Line s & q in Vertical_Line s implies LSeg (p,q) c= Vertical_Line s )
A1: Vertical_Line s = { p1 where p1 is Point of (TOP-REAL 2) : p1 `1 = s } by JORDAN6:def 6;
assume ( p in Vertical_Line s & q in Vertical_Line s ) ; :: thesis: LSeg (p,q) c= Vertical_Line s
then A2: ( p `1 = s & q `1 = s ) by JORDAN6:31;
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in LSeg (p,q) or u in Vertical_Line s )
assume A3: u in LSeg (p,q) ; :: thesis: u in Vertical_Line s
then reconsider p1 = u as Point of (TOP-REAL 2) ;
p1 `1 = s by A2, A3, GOBOARD7:5;
hence u in Vertical_Line s by A1; :: thesis: verum