let x be set ; :: thesis: for C being Coherence_Space st x in union C holds
{x} in C
let C be Coherence_Space; :: thesis: ( x in union C implies {x} in C )
assume x in union C ; :: thesis: {x} in C
then consider X being set such that
A1: x in X and
A2: X in C by TARSKI:def 4;
{x} c= X by A1, ZFMISC_1:31;
hence {x} in C by A2, CLASSES1:def 1; :: thesis: verum