:: deftheorem Def20 defines LinCoh COHSP_1:def 20 :
for C1, C2 being Coherence_Space
for b₃ being set holds
( b₃ = LinCoh (C1,C2) iff for x being set holds
( x in b₃ iff ex f being U-linear Function of C1,C2 st x = LinTrace f ) );