let x, y be object ; :: thesis: {x} c= {x,y}
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {x} or z in {x,y} )
assume z in {x} ; :: thesis: z in {x,y}
then z = x by TARSKI:def 1;
hence z in {x,y} by TARSKI:def 2; :: thesis: verum