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 ) ) ;
hence {} in C by Def1, ZFMISC_1:2; :: thesis: verum