let C be FormalContext; :: thesis: ( "\/" (([#] the carrier of (ConceptLattice C)),C) = Concept-with-all-Objects C & "/\" (([#] the carrier of (ConceptLattice C)),C) = Concept-with-all-Attributes C )
A1: @ (Concept-with-all-Attributes C) is_less_than [#] the carrier of (ConceptLattice C)
proof
let q be Element of (ConceptLattice C); :: according to LATTICE3:def 16 :: thesis: ( not q in [#] the carrier of (ConceptLattice C) or @ (Concept-with-all-Attributes C) [= q )
assume q in [#] the carrier of (ConceptLattice C) ; :: thesis: @ (Concept-with-all-Attributes C) [= q
( Concept-with-all-Attributes C is-SubConcept-of q @ & Concept-with-all-Attributes C = (@ (Concept-with-all-Attributes C)) @ ) by CONLAT_1:30, CONLAT_1:def 21;
hence @ (Concept-with-all-Attributes C) [= q by CONLAT_1:43; :: thesis: verum
end;
( "\/" ( the carrier of (ConceptLattice C),(ConceptLattice C)) = Top (ConceptLattice C) & ( for b being Element of (ConceptLattice C) st b is_less_than [#] the carrier of (ConceptLattice C) holds
b [= @ (Concept-with-all-Attributes C) ) ) by LATTICE3:50;
hence ( "\/" (([#] the carrier of (ConceptLattice C)),C) = Concept-with-all-Objects C & "/\" (([#] the carrier of (ConceptLattice C)),C) = Concept-with-all-Attributes C ) by A1, Th1, LATTICE3:34; :: thesis: verum