let C be FormalContext; :: thesis: for o being Object of C
for a being Attribute of C holds
( (gamma C) . o is FormalConcept of C & (delta C) . a is FormalConcept of C )
let o be Object of C; :: thesis: for a being Attribute of C holds
( (gamma C) . o is FormalConcept of C & (delta C) . a is FormalConcept of C )
let a be Attribute of C; :: thesis: ( (gamma C) . o is FormalConcept of C & (delta C) . a is FormalConcept of C )
ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) by CONLAT_1:def 20;
hence ( (gamma C) . o is FormalConcept of C & (delta C) . a is FormalConcept of C ) by CONLAT_1:def 15; :: thesis: verum