let C1, C2 be Coherence_Space; :: thesis: union (StabCoh (C1,C2)) = [:(Sub_of_Fin C1),(union C2):]
thus union (StabCoh (C1,C2)) c= [:(Sub_of_Fin C1),(union C2):] :: according to XBOOLE_0:def 10 :: thesis: [:(Sub_of_Fin C1),(union C2):] c= union (StabCoh (C1,C2))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (StabCoh (C1,C2)) or x in [:(Sub_of_Fin C1),(union C2):] )
assume x in union (StabCoh (C1,C2)) ; :: thesis: x in [:(Sub_of_Fin C1),(union C2):]
then consider a being set such that
A1: x in a and
A2: a in StabCoh (C1,C2) by TARSKI:def 4;
ex f being U-stable Function of C1,C2 st a = Trace f by A2, Def18;
then a c= [:(Sub_of_Fin C1),(union C2):] by Th46;
hence x in [:(Sub_of_Fin C1),(union C2):] by A1; :: thesis: verum
end;
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in [:(Sub_of_Fin C1),(union C2):] or [x,y] in union (StabCoh (C1,C2)) )
assume A3: [x,y] in [:(Sub_of_Fin C1),(union C2):] ; :: thesis: [x,y] in union (StabCoh (C1,C2))
then A4: y in union C2 by ZFMISC_1:87;
reconsider x = x as set by TARSKI:1;
A5: x in Sub_of_Fin C1 by A3, ZFMISC_1:87;
then x is finite by Def3;
then ex f being U-stable Function of C1,C2 st Trace f = {[x,y]} by A5, A4, Th42;
then ( [x,y] in {[x,y]} & {[x,y]} in StabCoh (C1,C2) ) by Def18, TARSKI:def 1;
hence [x,y] in union (StabCoh (C1,C2)) by TARSKI:def 4; :: thesis: verum