let a, b 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 ) implies {a,b} 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 ) ) ; :: thesis: {a,b} c= {1,2,3,4}
for x being object st x in {a,b} holds
x in {1,2,3,4}

proof

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

end;

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