let a be set ; :: thesis: ( ( a = 1 or a = 2 or a = 3 or a = 4 ) implies {a} c= {1,2,3,4} )
assume A1: ( a = 1 or a = 2 or a = 3 or a = 4 ) ; :: thesis: {a} c= {1,2,3,4}
for x being object st x in {a} holds
x in {1,2,3,4}
proof
let x be object ; :: thesis: ( x in {a} implies x in {1,2,3,4} )
assume x in {a} ; :: thesis: x in {1,2,3,4}
then x = a by TARSKI:def 1;
hence x in {1,2,3,4} by ENUMSET1:def 2, A1; :: thesis: verum
end;
hence {a} c= {1,2,3,4} ; :: thesis: verum