let C be FormalContext; :: thesis: ( Bottom (ConceptLattice C) = Concept-with-all-Attributes C & Top (ConceptLattice C) = Concept-with-all-Objects C )
A1: (@ (Concept-with-all-Objects C)) @ = Concept-with-all-Objects C by CONLAT_1:def 21;
A2: for a being Element of (ConceptLattice C) holds a [= @ (Concept-with-all-Objects C)
proof
let a be Element of (ConceptLattice C); :: thesis: a [= @ (Concept-with-all-Objects C)
a @ is-SubConcept-of (@ (Concept-with-all-Objects C)) @ by A1, CONLAT_1:30;
hence a [= @ (Concept-with-all-Objects C) by CONLAT_1:43; :: thesis: verum
end;
A3: for a being Element of (ConceptLattice C) holds
( (@ (Concept-with-all-Objects C)) "\/" a = @ (Concept-with-all-Objects C) & a "\/" (@ (Concept-with-all-Objects C)) = @ (Concept-with-all-Objects C) ) by A2, LATTICES:def 3;
A4: (@ (Concept-with-all-Attributes C)) @ = Concept-with-all-Attributes C by CONLAT_1:def 21;
A5: for a being Element of (ConceptLattice C) holds @ (Concept-with-all-Attributes C) [= a
proof
let a be Element of (ConceptLattice C); :: thesis: @ (Concept-with-all-Attributes C) [= a
(@ (Concept-with-all-Attributes C)) @ is-SubConcept-of a @ by A4, CONLAT_1:30;
hence @ (Concept-with-all-Attributes C) [= a by CONLAT_1:43; :: thesis: verum
end;
for a being Element of (ConceptLattice C) holds
( (@ (Concept-with-all-Attributes C)) "/\" a = @ (Concept-with-all-Attributes C) & a "/\" (@ (Concept-with-all-Attributes C)) = @ (Concept-with-all-Attributes C) ) by A5, LATTICES:4;
hence ( Bottom (ConceptLattice C) = Concept-with-all-Attributes C & Top (ConceptLattice C) = Concept-with-all-Objects C ) by A3, LATTICES:def 16, LATTICES:def 17; :: thesis: verum