let C be FormalContext; :: thesis: for CP being object holds
( CP in B-carrier C iff CP is strict FormalConcept of C )
let CP be object ; :: thesis: ( CP in B-carrier C iff CP is strict FormalConcept of C )
A1: ( CP is strict FormalConcept of C implies CP in B-carrier C )

proof

assume A2: CP is strict FormalConcept of C ; :: thesis: CP in B-carrier C
then reconsider CP = CP as FormalConcept of C ;
set I9 = the Intent of CP;
set E9 = the Extent of CP;
( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) by Def9;
hence CP in B-carrier C by A2; :: thesis: verum

end;

( CP in B-carrier C implies CP is strict FormalConcept of C )

proof

assume CP in B-carrier C ; :: thesis: CP is strict FormalConcept of C
then ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st
( CP = ConceptStr(# E,I #) & not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) ;
hence CP is strict FormalConcept of C by Def9; :: thesis: verum

end;

hence ( CP in B-carrier C iff CP is strict FormalConcept of C ) by A1; :: thesis: verum