(<=> (One-One ?R) (And (Binary-Relation ?R) (Function ?R) (Value-Type ?R Inverse Function) (Value-Cardinality ?R Inverse 1)))