:: deftheorem defines c= HEYTING1:def 1 :
for A being non empty set
for B, C being Element of Fin A holds
( B c= C iff for a being Element of A st a in B holds
a in C );