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