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;