set CP = the FormalConcept of C;
for X being set st X in { the FormalConcept of C} holds
X is FormalConcept of C by TARSKI:def 1;
hence ex b₁ being non empty set st
for X being set st X in b₁ holds
X is FormalConcept of C ; :: thesis: verum