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 set ; :: 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 & a in StabCoh C1,C2 ) by TARSKI:def 4;
ex f being U-stable Function of C1,C2 st a = Trace f by A1, Def19;
then a c= [:(Sub_of_Fin C1),(union C2):] by Th47;
hence x in [:(Sub_of_Fin C1),(union C2):] by A1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [:(Sub_of_Fin C1),(union C2):] or x in union (StabCoh C1,C2) )
assume x in [:(Sub_of_Fin C1),(union C2):] ; :: thesis: x in union (StabCoh C1,C2)
then A2: ( x = [(x `1 ),(x `2 )] & x `1 in Sub_of_Fin C1 & x `2 in union C2 ) by MCART_1:10, MCART_1:23;
then ( x `1 is finite & x `1 in C1 ) by Def3;
then ex f being U-stable Function of C1,C2 st Trace f = {x} by A2, Th43;
then ( x in {x} & {x} in StabCoh C1,C2 ) by Def19, TARSKI:def 1;
hence x in union (StabCoh C1,C2) by TARSKI:def 4; :: thesis: verum