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: "\/" the carrier of (ConceptLattice C),(ConceptLattice C) = Top (ConceptLattice C) by LATTICE3:51;
A2: @ (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
A3: Concept-with-all-Attributes C is-SubConcept-of q @ by CONLAT_1:34;
Concept-with-all-Attributes C = (@ (Concept-with-all-Attributes C)) @ by CONLAT_1:def 24;
hence @ (Concept-with-all-Attributes C) [= q by A3, CONLAT_1:47; :: thesis: verum

end;

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:def 16;
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, A2, Th1, LATTICE3:34; :: thesis: verum