let X, x be set ; :: thesis: ( x in FlatCoh X iff ( x = {} or ex y being set st
( x = {y} & y in X ) ) )

hereby :: thesis: ( ( x = {} or ex y being set st
( x = {y} & y in X ) ) implies x in FlatCoh X )

assume A1: x in FlatCoh X ; :: thesis: ( x <> {} implies ex z being set st
( x = {z} & z in X ) )
assume x <> {} ; :: thesis: ex z being set st
( x = {z} & z in X )
then reconsider y = x as non empty set ;
set z = the Element of y;
reconsider z = the Element of y as set ;
take z = z; :: thesis: ( x = {z} & z in X )
thus x = {z} :: thesis: z in X

proof

hereby :: according to XBOOLE_0:def 10,TARSKI:def 3 :: thesis: {z} c= x

let c be object ; :: thesis: ( c in x implies c in {z} )
assume c in x ; :: thesis: c in {z}
then [z,c] in id X by A1, COH_SP:def 3;
then c = z by RELAT_1:def 10;
hence c in {z} by TARSKI:def 1; :: thesis: verum

end;

thus {z} c= x by ZFMISC_1:31; :: thesis: verum

end;

[z,z] in id X by A1, COH_SP:def 3;
hence z in X by RELAT_1:def 10; :: thesis: verum

end;

A2: now :: thesis: ( ex a being set st
( x = {a} & a in X ) implies for y, z being set st y in x & z in x holds
[y,z] in id X )

given a being set such that A3: x = {a} and
A4: a in X ; :: thesis: for y, z being set st y in x & z in x holds
[y,z] in id X
let y, z be set ; :: thesis: ( y in x & z in x implies [y,z] in id X )
assume ( y in x & z in x ) ; :: thesis: [y,z] in id X
then ( y = a & z = a ) by A3, TARSKI:def 1;
hence [y,z] in id X by A4, RELAT_1:def 10; :: thesis: verum

end;

assume ( x = {} or ex y being set st
( x = {y} & y in X ) ) ; :: thesis: x in FlatCoh X
hence x in FlatCoh X by A2, COH_SP:1, COH_SP:def 3; :: thesis: verum