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