set C = LinCoh C1,C2;
consider f being U-linear Function of C1,C2;
LinTrace f in LinCoh C1,C2 by Def21;
hence not LinCoh C1,C2 is empty ; :: thesis: ( LinCoh C1,C2 is subset-closed & LinCoh C1,C2 is binary_complete )
thus LinCoh C1,C2 is subset-closed :: thesis: LinCoh C1,C2 is binary_complete

proof

let a, b be set ; :: according to CLASSES1:def 1 :: thesis: ( not a in LinCoh C1,C2 or not b c= a or b in LinCoh C1,C2 )
assume a in LinCoh C1,C2 ; :: thesis: ( not b c= a or b in LinCoh C1,C2 )
then A1: ex f being U-linear Function of C1,C2 st a = LinTrace f by Def21;
assume b c= a ; :: thesis: b in LinCoh C1,C2
then ex g being U-linear Function of C1,C2 st LinTrace g = b by A1, Th62;
hence b in LinCoh C1,C2 by Def21; :: thesis: verum

end;

let A be set ; :: according to COHSP_1:def 1 :: thesis: ( ( for a, b being set st a in A & b in A holds
a \/ b in LinCoh C1,C2 ) implies union A in LinCoh C1,C2 )
assume A2: for a, b being set st a in A & b in A holds
a \/ b in LinCoh C1,C2 ; :: thesis: union A in LinCoh C1,C2

now

let x, y be set ; :: thesis: ( x in A & y in A implies ex f being U-linear Function of C1,C2 st x \/ y = LinTrace f )
assume ( x in A & y in A ) ; :: thesis: ex f being U-linear Function of C1,C2 st x \/ y = LinTrace f
then x \/ y in LinCoh C1,C2 by A2;
hence ex f being U-linear Function of C1,C2 st x \/ y = LinTrace f by Def21; :: thesis: verum

end;

then ex f being U-linear Function of C1,C2 st union A = LinTrace f by Th63;
hence union A in LinCoh C1,C2 by Def21; :: thesis: verum