for X being set st X in B-carrier C holds
X is FormalConcept of C

proof

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

end;

hence B-carrier C is Set-of-FormalConcepts of C by Def14; :: thesis: verum