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

now :: thesis: ( ( the Extent of CS is empty & not CS is empty ) or ( not the Extent of CS is empty & not CS is empty ) )

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

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

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

end;

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

hence not CS is empty ; :: thesis: verum

end;

end;

end;

hence not CS is empty ; :: thesis: verum