let p, q be Point of (TOP-REAL 2); :: thesis: ( p <> q implies LSeg (p,q) = { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) } )
assume A1: p <> q ; :: thesis: LSeg (p,q) = { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) }
thus LSeg (p,q) c= { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) } :: according to XBOOLE_0:def 10 :: thesis: { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) } c= LSeg (p,q)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in LSeg (p,q) or a in { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) } )
assume A2: a in LSeg (p,q) ; :: thesis: a in { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) }
then reconsider a9 = a as Point of (TOP-REAL 2) ;
A3: LE p,a9,p,q by A1, A2, Th10;
LE a9,q,p,q by A1, A2, Th11;
hence a in { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) } by A3; :: thesis: verum

end;

thus { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) } c= LSeg (p,q) :: thesis: verum

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) } or a in LSeg (p,q) )
assume a in { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) } ; :: thesis: a in LSeg (p,q)
then ex a9 being Point of (TOP-REAL 2) st
( a9 = a & LE p,a9,p,q & LE a9,q,p,q ) ;
hence a in LSeg (p,q) ; :: thesis: verum

end;