let C be FormalContext; :: thesis: ( "\/" (({} (ConceptLattice C)),C) = Concept-with-all-Attributes C & "/\" (({} (ConceptLattice C)),C) = Concept-with-all-Objects C )
A1: 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)
( b @ is-SubConcept-of Concept-with-all-Objects C & Concept-with-all-Objects C = (@ (Concept-with-all-Objects C)) @ ) by CONLAT_1:30, CONLAT_1:def 21;
hence b [= @ (Concept-with-all-Objects C) by CONLAT_1:43; :: thesis: verum

end;

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