theorem :: FOMODEL0:67

for Y being set
for U being non empty set
for x, y being Element of U holds
not ( ( x in Y implies y in Y ) & ( y in Y implies x in Y ) & not [((chi (Y,U)) . x),((chi (Y,U)) . y)] in id BOOLEAN ) by Lm54;