defpred S₁[ Element of M] means x tolerates $1;
{ y where y is Element of M : S₁[y] } c= the carrier of M from FRAENKEL:sch 10();
hence { y where y is Element of M : x tolerates y } is Subset of M ; :: thesis: verum