theorem :: GLIBPRE0:3

for x, y being object holds
( {x,y} \ { the Element of {x,y}} = {} iff x = y )