let C be Coherence_Space; :: thesis: {} in C
A1: {} c= C by XBOOLE_1:2;
for a, b being set st a in {} & b in {} holds
a \/ b in C ;
hence {} in C by A1, Def2, ZFMISC_1:2; :: thesis: verum