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