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

proof

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

end;

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

proof

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

end;

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