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

let o be object ; :: thesis: ( o in {a,b} implies b₁ in the carrier of V )
assume o in {a,b} ; :: thesis: b₁ in the carrier of V

per cases then ( o = a or o = b ) by TARSKI:def 2;

suppose o = a ; :: thesis: b₁ in the carrier of V

hence o in the carrier of V ; :: thesis: verum

end;

suppose o = b ; :: thesis: b₁ in the carrier of V

hence o in the carrier of V ; :: thesis: verum

end;

end;

end;

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