let C be FormalContext; :: thesis: for O being Subset of the carrier of C
for A being Subset of the carrier' of C st ConceptStr(# O,A #) is FormalConcept of C holds
ConceptStr(# O,A #) .: is FormalConcept of C .:
let O be Subset of the carrier of C; :: thesis: for A being Subset of the carrier' of C st ConceptStr(# O,A #) is FormalConcept of C holds
ConceptStr(# O,A #) .: is FormalConcept of C .:
let A be Subset of the carrier' of C; :: thesis: ( ConceptStr(# O,A #) is FormalConcept of C implies ConceptStr(# O,A #) .: is FormalConcept of C .: )
assume ConceptStr(# O,A #) is FormalConcept of C ; :: thesis: ConceptStr(# O,A #) .: is FormalConcept of C .:
then reconsider CP = ConceptStr(# O,A #) as strict FormalConcept of C ;
CP .: is strict FormalConcept of C .: ;
hence ConceptStr(# O,A #) .: is FormalConcept of C .: ; :: thesis: verum