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
; ( StabCoh (C1,C2) is subset-closed & StabCoh (C1,C2) is binary_complete )
thus
StabCoh (C1,C2) is subset-closed
StabCoh (C1,C2) is binary_complete proof
let a,
b be
set ;
CLASSES1:def 1 ( not a in StabCoh (C1,C2) or not b c= a or b in StabCoh (C1,C2) )
assume
a in StabCoh (
C1,
C2)
;
( 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
;
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;
verum
end;
let A be set ; COHSP_1:def 1 ( ( 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)
; union A in StabCoh (C1,C2)
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; verum