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