let C be FormalContext; :: thesis: ( "\/" ({} (ConceptLattice C)),C = Concept-with-all-Attributes C & "/\" ({} (ConceptLattice C)),C = Concept-with-all-Objects C )
A1: "\/" ({} (ConceptLattice C)),C = Bottom (ConceptLattice C) by LATTICE3:50;
for q being Element of (ConceptLattice C) st q in {} holds
@ (Concept-with-all-Objects C) [= q ;
then A2: @ (Concept-with-all-Objects C) is_less_than {} by LATTICE3:def 16;
for b being Element of (ConceptLattice C) st b is_less_than {} holds
b [= @ (Concept-with-all-Objects C)

proof

let b be Element of (ConceptLattice C); :: thesis: ( b is_less_than {} implies b [= @ (Concept-with-all-Objects C) )
assume b is_less_than {} ; :: thesis: b [= @ (Concept-with-all-Objects C)
A3: b @ is-SubConcept-of Concept-with-all-Objects C by CONLAT_1:34;
Concept-with-all-Objects C = (@ (Concept-with-all-Objects C)) @ by CONLAT_1:def 24;
hence b [= @ (Concept-with-all-Objects C) by A3, CONLAT_1:47; :: thesis: verum

end;

hence ( "\/" ({} (ConceptLattice C)),C = Concept-with-all-Attributes C & "/\" ({} (ConceptLattice C)),C = Concept-with-all-Objects C ) by A1, A2, Th1, LATTICE3:34; :: thesis: verum