let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1 being Point of (TOP-REAL 2) st q1 in P holds

LE q1,q1,P,p1,p2

let p1, p2, q1 be Point of (TOP-REAL 2); :: thesis: ( q1 in P implies LE q1,q1,P,p1,p2 )

assume A1: q1 in P ; :: thesis: LE q1,q1,P,p1,p2

then reconsider P = P as non empty Subset of (TOP-REAL 2) ;

LE q1,q1,P,p1,p2

let p1, p2, q1 be Point of (TOP-REAL 2); :: thesis: ( q1 in P implies LE q1,q1,P,p1,p2 )

assume A1: q1 in P ; :: thesis: LE q1,q1,P,p1,p2

then reconsider P = P as non empty Subset of (TOP-REAL 2) ;

now :: thesis: for g being Function of I[01],((TOP-REAL 2) | P)

for s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds

s1 <= s2

hence
LE q1,q1,P,p1,p2
by A1; :: thesis: verumfor s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds

s1 <= s2

let g be Function of I[01],((TOP-REAL 2) | P); :: thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds

s1 <= s2

let s1, s2 be Real; :: thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q1 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )

assume that

A2: g is being_homeomorphism and

g . 0 = p1 and

g . 1 = p2 and

A3: g . s1 = q1 and

A4: ( 0 <= s1 & s1 <= 1 ) and

A5: g . s2 = q1 and

A6: ( 0 <= s2 & s2 <= 1 ) ; :: thesis: s1 <= s2

A7: g is one-to-one by A2, TOPS_2:def 5;

( s1 in the carrier of I[01] & s2 in the carrier of I[01] ) by A4, A6, BORSUK_1:43;

hence s1 <= s2 by A3, A5, A7, FUNCT_2:19; :: thesis: verum

end;s1 <= s2

let s1, s2 be Real; :: thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q1 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )

assume that

A2: g is being_homeomorphism and

g . 0 = p1 and

g . 1 = p2 and

A3: g . s1 = q1 and

A4: ( 0 <= s1 & s1 <= 1 ) and

A5: g . s2 = q1 and

A6: ( 0 <= s2 & s2 <= 1 ) ; :: thesis: s1 <= s2

A7: g is one-to-one by A2, TOPS_2:def 5;

( s1 in the carrier of I[01] & s2 in the carrier of I[01] ) by A4, A6, BORSUK_1:43;

hence s1 <= s2 by A3, A5, A7, FUNCT_2:19; :: thesis: verum