theorem :: TARSKI_0:3

for x, y being object ex z being set st
for a being object holds
( a in z iff ( a = x or a = y ) ) ;