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 object ; :: 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 and
A2: y in FlatCoh X by TARSKI:def 4;
ex z being set st
( y = {z} & z in X ) by A1, A2, Th1;
hence x in X by A1, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: 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