x,y:T. R(x;y) 
R(y;x)T:Type, R:(T
TProp). Connex(T;x,y.R(x,y)) 
Prop| Who Cites connex? | |
| connex | Def Connex(T;x,y.R(x;y)) == x,y:T. R(x;y) R(y;x) |
| Thm* T:Type, R:(TTProp). Connex(T;x,y.R(x,y)) Prop |
| Syntax: | Connex(T;x,y.R(x;y)) | has structure: | connex(T; x,y.R(x;y)) |
About:
 |  |  |  |  |  |  |