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

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

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

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

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

end;

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

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

end;

end;

end;

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