let a, b be set ; ( ( 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 ) )
; {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 ;
( x in {a,b} implies x in {1,2,3,4} )
assume
x in {a,b}
;
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;
verum
end;
hence
{a,b} c= {1,2,3,4}
; verum