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