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;
end;
end;
hence not CS is empty ; :: thesis: verum