let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds Segment P,p1,p2,q1,q2 = { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) }
let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: Segment P,p1,p2,q1,q2 = { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) }
thus
Segment P,p1,p2,q1,q2 c= { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) }
:: according to XBOOLE_0:def 10 :: thesis: { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } c= Segment P,p1,p2,q1,q2proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in Segment P,p1,p2,q1,q2 or x in { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } )
assume
x in Segment P,
p1,
p2,
q1,
q2
;
:: thesis: x in { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) }
then A1:
(
x in R_Segment P,
p1,
p2,
q1 &
x in L_Segment P,
p1,
p2,
q2 )
by XBOOLE_0:def 4;
then consider q being
Point of
(TOP-REAL 2) such that A2:
(
q = x &
LE q1,
q,
P,
p1,
p2 )
;
consider p being
Point of
(TOP-REAL 2) such that A3:
(
p = x &
LE p,
q2,
P,
p1,
p2 )
by A1;
thus
x in { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) }
by A2, A3;
:: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } or x in Segment P,p1,p2,q1,q2 )
assume
x in { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) }
; :: thesis: x in Segment P,p1,p2,q1,q2
then consider q being Point of (TOP-REAL 2) such that
A4:
( q = x & LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 )
;
A5:
x in R_Segment P,p1,p2,q1
by A4;
x in L_Segment P,p1,p2,q2
by A4;
hence
x in Segment P,p1,p2,q1,q2
by A5, XBOOLE_0:def 4; :: thesis: verum