let C be FormalContext; :: thesis: for CS being ConceptStr of C st (ObjectDerivation C) . the Extent of CS = the Intent of CS & (AttributeDerivation C) . the Intent of CS = the Extent of CS holds
not CS is empty
let CS be ConceptStr of C; :: thesis: ( (ObjectDerivation C) . the Extent of CS = the Intent of CS & (AttributeDerivation C) . the Intent of CS = the Extent of CS implies not CS is empty )
assume A1: ( (ObjectDerivation C) . the Extent of CS = the Intent of CS & (AttributeDerivation C) . the Intent of CS = the Extent 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:18;
hence not CS is empty by CONLAT_1:def 11; :: 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 11; :: thesis: verum

end;

end;