theorem :: FACIRC_2:2

for x, y, z being set holds
( x <> [<*x,y*>,z] & y <> [<*x,y*>,z] )