Q == P + Q
a 
x b
T:Type, a,b:Collection(T). (a + b) Collection(T) c == c(x)T:Type, x:T, c:Collection(T). x c Prop| Who Cites pred and? | |
| pred_and | Def P Q == P + Q |
| col_add |
Def (a + b)(x) == x a x b |
| Thm* T:Type, a,b:Collection(T). (a + b) Collection(T) | |
| col_member |
Def x c == c(x) |
| Thm* T:Type, x:T, c:Collection(T). x c Prop |
| Syntax: | P Q | has structure: | pred_and(P; Q) |
About:
 |  |  |  |  |  |  |