:: deftheorem defines Ext HILB10_7:def 2 :
for X being set
for a, b being object holds Ext (X,a,b) = { (A \/ {b}) where A is Element of X : a in A } \/ { A where A is Element of X : ( not a in A & A in X ) } ;