Step
*
2
of Lemma
ss-id_wf
.....set predicate..... 
1. X : SeparationSpace
⊢ ss-function(X;X;ss-id())
BY
{ (RepUR ``ss-id ss-function`` 0 THEN Auto) }
Latex:
Latex:
.....set  predicate..... 
1.  X  :  SeparationSpace
\mvdash{}  ss-function(X;X;ss-id())
By
Latex:
(RepUR  ``ss-id  ss-function``  0  THEN  Auto)
Home
Index