now

let x be set ; :: thesis: ( x in { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) } implies x in the carrier of S )
assume x in { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) } ; :: thesis: x in the carrier of S
then ex t being Real st
( x = p + (t * (q - p)) & 0 < t & t < 1 ) ;
hence x in the carrier of S ; :: thesis: verum

end;

hence { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) } is Subset of S by TARSKI:def 3; :: thesis: verum