for C being FormalContext
for CP being FormalConcept of C holds
( CP is-SubConcept-of Concept-with-all-Objects C & Concept-with-all-Attributes C is-SubConcept-of CP )