theorem Th31: :: ZFMISC_1:32

for x1, x2 being object
for Z being set holds
( {x1,x2} c= Z iff ( x1 in Z & x2 in Z ) )