Reversed relation
Set
context
$ R\in\text{Rel}(X,Y) $
definiendum
$ \langle x,y \rangle \in R^\smile $
postulate
$ \langle y,x \rangle \in R $
Ramifications
Reference
Mizar files:
RELAT_1
Parents
Context
Binary relation