let S be RealLinearSpace; :: thesis: for p, q being Point of S st p <> q holds
].p,q.[ = { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) }
let p, q be Point of S; :: thesis: ( p <> q implies ].p,q.[ = { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) } )
assume AS1: p <> q ; :: thesis: ].p,q.[ = { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) }
set A = { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) } ;
for x being object holds
( x in ].p,q.[ iff x in { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) } )
proof
let x be object ; :: thesis: ( x in ].p,q.[ iff x in { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) } )
hereby :: thesis: ( x in { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) } implies x in ].p,q.[ )
assume x in ].p,q.[ ; :: thesis: x in { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) }
then P1: ( x in [.p,q.] & not x in {p,q} ) by XBOOLE_0:def 5;
then x in { (((1 - r) * p) + (r * q)) where r is Real : ( 0 <= r & r <= 1 ) } by RLTOPSP1:def 2;
then consider t being Real such that
P2: ( x = ((1 - t) * p) + (t * q) & 0 <= t & t <= 1 ) ;
P3: x = p + (t * (q - p)) by P2, Lm2;
P4: 0 <> t
proof
assume t = 0 ; :: thesis: contradiction
then x = p + (0. S) by P3, RLVECT_1:10
.= p by RLVECT_1:4 ;
hence contradiction by P1, TARSKI:def 2; :: thesis: verum
end;
1 <> t
proof
assume t = 1 ; :: thesis: contradiction
then x = p + (q - p) by P3, RLVECT_1:def 8
.= q - (p - p) by RLVECT_1:29
.= q - (0. S) by RLVECT_1:15
.= q by RLVECT_1:13 ;
hence contradiction by P1, TARSKI:def 2; :: thesis: verum
end;
then ( 0 < t & t < 1 ) by P2, P4, XXREAL_0:1;
hence x in { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) } by P3; :: thesis: verum
end;
assume x in { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) } ; :: thesis: x in ].p,q.[
then consider t being Real such that
P4: ( x = p + (t * (q - p)) & 0 < t & t < 1 ) ;
x = ((1 - t) * p) + (t * q) by Lm2, P4;
then x in { (((1 - r) * p) + (r * q)) where r is Real : ( 0 <= r & r <= 1 ) } by P4;
then P5: x in [.p,q.] by RLTOPSP1:def 2;
P6: x <> p
proof
assume x = p ; :: thesis: contradiction
then P7: 0. S = ((t * (q - p)) + p) - p by P4, RLVECT_1:15
.= (t * (q - p)) + (p - p) by RLVECT_1:28
.= (t * (q - p)) + (0. S) by RLVECT_1:15
.= t * (q - p) by RLVECT_1:4 ;
q - p <> 0. S by AS1, RLVECT_1:21;
hence contradiction by P4, P7, RLVECT_1:11; :: thesis: verum
end;
x <> q
proof
assume x = q ; :: thesis: contradiction
then q - p = (t * (q - p)) + (p - p) by P4, RLVECT_1:28
.= (t * (q - p)) + (0. S) by RLVECT_1:15
.= t * (q - p) by RLVECT_1:4 ;
then 1 * (q - p) = t * (q - p) by RLVECT_1:def 8;
then (1 * (q - p)) - (t * (q - p)) = 0. S by RLVECT_1:15;
then P7: (1 - t) * (q - p) = 0. S by RLVECT_1:35;
q - p <> 0. S by AS1, RLVECT_1:21;
then 1 - t = 0 by RLVECT_1:11, P7;
hence contradiction by P4; :: thesis: verum
end;
then not x in {p,q} by P6, TARSKI:def 2;
hence x in ].p,q.[ by P5, XBOOLE_0:def 5; :: thesis: verum
end;
hence ].p,q.[ = { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) } by TARSKI:2; :: thesis: verum