let s be Element of S; :: thesis: s is FormalConcept of C
s is Element of B-carrier C ;
hence s is FormalConcept of C ; :: thesis: verum