A1: { t where t is FinSequence of S : s,t -are_prob_equivalent } c= S *

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { t where t is FinSequence of S : s,t -are_prob_equivalent } or x in S * )
assume x in { t where t is FinSequence of S : s,t -are_prob_equivalent } ; :: thesis: x in S *
then ex t being FinSequence of S st
( x = t & s,t -are_prob_equivalent ) ;
hence x in S * by FINSEQ_1:def 11; :: thesis: verum

end;

s in { t where t is FinSequence of S : s,t -are_prob_equivalent } ;
hence { t where t is FinSequence of S : s,t -are_prob_equivalent } is non empty Subset of (S * ) by A1; :: thesis: verum