let a, b be set ; :: thesis: {a} c= {a,b}

now

let u be set ; :: thesis: ( u in {a} implies u in {a,b} )
assume u in {a} ; :: thesis: u in {a,b}
then u = a by TARSKI:def 1;
hence u in {a,b} by TARSKI:def 2; :: thesis: verum

end;

hence {a} c= {a,b} by TARSKI:def 3; :: thesis: verum