now :: thesis: for o being object st o in {a} holds
o in the carrier of V

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

end;

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