set C = StabCoh C1,C2;
consider f being U-stable Function of C1,C2;
Trace f in StabCoh C1,C2 by Def19;
hence not StabCoh C1,C2 is empty ; :: thesis: ( StabCoh C1,C2 is subset-closed & StabCoh C1,C2 is binary_complete )
thus StabCoh C1,C2 is subset-closed :: thesis: StabCoh C1,C2 is binary_complete

proof

let a, b be set ; :: according to CLASSES1:def 1 :: thesis: ( not a in StabCoh C1,C2 or not b c= a or b in StabCoh C1,C2 )
assume a in StabCoh C1,C2 ; :: thesis: ( not b c= a or b in StabCoh C1,C2 )
then A1: ex f being U-stable Function of C1,C2 st a = Trace f by Def19;
assume b c= a ; :: thesis: b in StabCoh C1,C2
then ex g being U-stable Function of C1,C2 st Trace g = b by A1, Th45;
hence b in StabCoh C1,C2 by Def19; :: 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 StabCoh C1,C2 ) implies union A in StabCoh C1,C2 )
assume A2: for a, b being set st a in A & b in A holds
a \/ b in StabCoh C1,C2 ; :: thesis: union A in StabCoh C1,C2

now

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

end;

then ex f being U-stable Function of C1,C2 st union A = Trace f by Th46;
hence union A in StabCoh C1,C2 by Def19; :: thesis: verum