:: deftheorem defines Cauchy YELLOW19:def 5 :
for S being non empty 1-sorted
for N being non empty NetStr over S holds
( N is Cauchy iff for A being Subset of S holds
( N is_eventually_in A or N is_eventually_in A ` ) );