let C be FormalContext; :: thesis: 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 )
let CP be FormalConcept of C; :: thesis: ( CP is-SubConcept-of Concept-with-all-Objects C & Concept-with-all-Attributes C is-SubConcept-of CP )
A1: ( the carrier' of C = the Intent of (Concept-with-all-Attributes C) & the Intent of CP c= the carrier' of C ) by Th23;
( the carrier of C = the Extent of (Concept-with-all-Objects C) & the Extent of CP c= the carrier of C ) by Th23;
hence ( CP is-SubConcept-of Concept-with-all-Objects C & Concept-with-all-Attributes C is-SubConcept-of CP ) by A1, Th28; :: thesis: verum