let a, b be set ; :: thesis: {a} c= {a,b}
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in {a} or 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