now :: thesis: for x being object st x in {a} holds
x in the carrier of R

let x be object ; :: thesis: ( x in {a} implies x in the carrier of R )
assume x in {a} ; :: thesis: x in the carrier of R
then x = a by TARSKI:def 1;
hence x in the carrier of R ; :: thesis: verum

end;

hence {a} is Subset of R by TARSKI:def 3; :: thesis: verum