IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Subtypes by Comprehension - sometimes called "set types"
{x:A| B(x) } is the subtype of A restricted to the PropertyB(x)(xA).
It is the type of aA such that B(a).
Note that "a {x:A| B(x) }" is not equivalent to "B(a)", since "B(a)" can be assigned a meaning for any aA, but "a {x:A| B(x) }" is not assigned a meaning unless it is true, i.e., when "B(a)" is true.