:: deftheorem Def18 defines StabCoh COHSP_1:def 18 :
for C1, C2 being Coherence_Space
for b₃ being set holds
( b₃ = StabCoh (C1,C2) iff for x being set holds
( x in b₃ iff ex f being U-stable Function of C1,C2 st x = Trace f ) );