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

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in LSeg p,q or a in { p1 where p1 is Point of : ( 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 : ( LE p,p1,p,q & LE p1,q,p,q ) }
then reconsider a' = a as Point of ;
A3: LE p,a',p,q by A1, A2, Th10;
LE a',q,p,q by A1, A2, Th11;
hence a in { p1 where p1 is Point of : ( LE p,p1,p,q & LE p1,q,p,q ) } by A3; :: thesis: verum

end;

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

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { p1 where p1 is Point of : ( 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 : ( LE p,p1,p,q & LE p1,q,p,q ) } ; :: thesis: a in LSeg p,q
then ex a' being Point of st
( a' = a & LE p,a',p,q & LE a',q,p,q ) ;
hence a in LSeg p,q by JORDAN3:65; :: thesis: verum

end;