theorem Th15: :: ZF_LANG:15

for x, y being Variable holds
( (x '=' y) . 1 = 0 & (x 'in' y) . 1 = 1 )