set C = LinCoh (C1,C2);
set f = the U-linear Function of C1,C2;
LinTrace the U-linear Function of C1,C2 in LinCoh (C1,C2) by Def20;
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 Def20;
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, Th61;
hence b in LinCoh (C1,C2) by Def20; :: 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 :: thesis: for x, y being set st x in A & y in A holds
ex f being U-linear Function of C1,C2 st x \/ y = LinTrace f
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 Def20; :: thesis: verum
end;
then ex f being U-linear Function of C1,C2 st union A = LinTrace f by Th62;
hence union A in LinCoh (C1,C2) by Def20; :: thesis: verum