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;
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;
then A3: ConceptLattice C is upper-bounded by LATTICES:def 14;
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;
then ConceptLattice C is lower-bounded by LATTICES:def 13;
hence ConceptLattice C is bounded by A3; :: thesis: verum