let C be Coherence_Space; :: thesis: ( union C in C implies C = bool (union C) )
assume A1: union C in C ; :: thesis: C = bool (union C)
thus C c= bool (union C) by ZFMISC_1:82; :: according to XBOOLE_0:def 10 :: thesis: bool (union C) c= C
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in bool (union C) or x in C )
assume x in bool (union C) ; :: thesis: x in C
hence x in C by A1, CLASSES1:def 1; :: thesis: verum