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,qproof
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 (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 a' =
a as
Point of
(TOP-REAL 2) ;
(
LE p,
a',
p,
q &
LE a',
q,
p,
q )
by A1, A2, Th10, Th11;
hence
a in { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) }
;
:: 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: verumproof
let a be
set ;
:: 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 consider a' being
Point of
(TOP-REAL 2) such that A3:
(
a' = a &
LE p,
a',
p,
q &
LE a',
q,
p,
q )
;
thus
a in LSeg p,
q
by A3, JORDAN3:65;
:: thesis: verum
end;