let C be FormalContext; :: thesis: for CS being ConceptStr over C st (ObjectDerivation C) . the Extent of CS = the Intent of CS holds
not CS is empty
let CS be ConceptStr over C; :: thesis: ( (ObjectDerivation C) . the Extent of CS = the Intent of CS implies not CS is empty )
assume A1: (ObjectDerivation C) . the Extent of CS = the Intent of CS ; :: thesis: not CS is empty

per cases ( the Extent of CS is empty or not the Extent of CS is empty ) ;

suppose the Extent of CS is empty ; :: thesis: not CS is empty

then the Intent of CS = the carrier' of C by A1, CONLAT_1:17;
hence not CS is empty by CONLAT_1:def 8; :: thesis: verum

end;

suppose not the Extent of CS is empty ; :: thesis: not CS is empty

hence not CS is empty by CONLAT_1:def 8; :: thesis: verum

end;

end;