set C = StabCoh (C1,C2);
set f = the U-stable Function of C1,C2;
Trace the U-stable Function of C1,C2 in StabCoh (C1,C2) by Def18;
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 Def18;
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, Th44;
hence b in StabCoh (C1,C2) by Def18; :: 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 :: thesis: for x, y being set st x in A & y in A holds
ex f being U-stable Function of C1,C2 st x \/ y = Trace f

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 Def18; :: thesis: verum

end;

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