for x being object st x in {1,2} holds
x in {1,2,3}

proof

let x be object ; :: thesis: ( x in {1,2} implies x in {1,2,3} )
assume x in {1,2} ; :: thesis: x in {1,2,3}
then ( x = 1 or x = 2 ) by TARSKI:def 2;
hence x in {1,2,3} by ENUMSET1:def 1; :: thesis: verum

end;

then T1: {1,2} c= {1,2,3} ;
{1,2} <> {1,2,3}

proof

3 in {1,2,3} by ENUMSET1:def 1;
hence {1,2} <> {1,2,3} by TARSKI:def 2; :: thesis: verum

end;

hence {1,2} c< {1,2,3} by T1; :: thesis: verum