| Who Cites rel 1 1 b? |
|
rel_1_1_b | Def 1-1 x A,y B. R(x;y)
Def == x,x':A, y,y':B. R(x;y) & R(x';y')  (x = x'  y = y') |
|
| Thm* A,B:Type, R:(A B Type). (1-1 x A,y B. R(x;y)) Type |
|
iff | Def P  Q == (P  Q) & (P  Q) |
|
| Thm* A,B:Prop. (A  B) Prop |
|
rev_implies | Def P  Q == Q  P |
|
| Thm* A,B:Prop. (A  B) Prop |