let X be set ; :: thesis: union (FlatCoh X) = X

hereby :: according to XBOOLE_0:def 10,TARSKI:def 3 :: thesis: X c= union (FlatCoh X)

let x be set ; :: thesis: ( x in union (FlatCoh X) implies x in X )
assume x in union (FlatCoh X) ; :: thesis: x in X
then consider y being set such that
A1: ( x in y & y in FlatCoh X ) by TARSKI:def 4;
consider z being set such that
A2: ( y = {z} & z in X ) by A1, Th1;
thus x in X by A1, A2, TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in union (FlatCoh X) )
assume x in X ; :: thesis: x in union (FlatCoh X)
then ( x in {x} & {x} in FlatCoh X ) by Th1, TARSKI:def 1;
hence x in union (FlatCoh X) by TARSKI:def 4; :: thesis: verum