theorem :: POLYVIE1:1

for a, b being object holds
( not a <> b or canFS {a,b} = <*a,b*> or canFS {a,b} = <*b,a*> )