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:34, CONLAT_1:def 24;
hence @ (Concept-with-all-Attributes C) [= q by CONLAT_1:47; :: 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:51, 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, Th1, LATTICE3:34; :: thesis: verum