let S be RealLinearSpace; :: thesis: for p, q being Point of S holds ].p,q.[ c= [.p,q.]
let p, q be Point of S; :: thesis: ].p,q.[ c= [.p,q.]

now

let z be set ; :: thesis: ( z in ].p,q.[ implies z in [.p,q.] )
assume z in ].p,q.[ ; :: thesis: z in [.p,q.]
then consider z1 being Real such that
AA: ( z = p + (z1 * (q - p)) & 0 < z1 & z1 < 1 ) ;
z = ((1 - z1) * p) + (z1 * q) by AA, LmX;
then z in { (((1 - r) * p) + (r * q)) where r is Real : ( 0 <= r & r <= 1 ) } by AA;
hence z in [.p,q.] by RLTOPSP1:def 2; :: thesis: verum

end;

hence ].p,q.[ c= [.p,q.] by TARSKI:def 3; :: thesis: verum