x,y:T. 
(R(x;y) & R(y;x))T:Type, R:(T
TProp). StAntiSym(T;x,y.R(x,y)) 
PropA == A 
FalseA:Prop. (A) Prop| No other cites to report in MarkB_generic | |
| st_anti_sym | Def StAntiSym(T;x,y.R(x;y)) == x,y:T. (R(x;y) & R(y;x)) |
| Thm* T:Type, R:(TTProp). StAntiSym(T;x,y.R(x,y)) Prop | |
| not | Def A == A False |
| Thm* A:Prop. (A) Prop |
| Syntax: | StAntiSym(T;x,y.R(x;y)) | has structure: | st_anti_sym(T; x,y.R(x;y)) |
About:
 |  |  |  |  |  |  |  |  |