let a, b, c be set ; :: thesis: ( ( a = 1 or a = 2 or a = 3 or a = 4 ) & ( b = 1 or b = 2 or b = 3 or b = 4 ) & ( c = 1 or c = 2 or c = 3 or c = 4 ) implies {a,b,c} c= {1,2,3,4} )
assume A1: ( ( a = 1 or a = 2 or a = 3 or a = 4 ) & ( b = 1 or b = 2 or b = 3 or b = 4 ) & ( c = 1 or c = 2 or c = 3 or c = 4 ) ) ; :: thesis: {a,b,c} c= {1,2,3,4}
for x being object st x in {a,b,c} holds
x in {1,2,3,4}

proof

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

end;

hence {a,b,c} c= {1,2,3,4} ; :: thesis: verum