now :: thesis: for x being object st x in {y1,y2,y3} holds
x in Y

let x be object ; :: thesis: ( x in {y1,y2,y3} implies b₁ in Y )
assume x in {y1,y2,y3} ; :: thesis: b₁ in Y

per cases then ( x = y1 or x = y2 or x = y3 ) by ENUMSET1:def 1;

suppose x = y1 ; :: thesis: b₁ in Y

hence x in Y ; :: thesis: verum

end;

suppose x = y2 ; :: thesis: b₁ in Y

hence x in Y ; :: thesis: verum

end;

suppose x = y3 ; :: thesis: b₁ in Y

hence x in Y ; :: thesis: verum

end;

end;

end;

hence {y1,y2,y3} is Subset of Y by TARSKI:def 3; :: thesis: verum