:: deftheorem Def3 defines FinMeetCl CANTOR_1:def 3 :
for X being set
for A, b₃ being Subset-Family of X holds
( b₃ = FinMeetCl A iff for x being Subset of X holds
( x in b₃ iff ex Y being Subset-Family of X st
( Y c= A & Y is finite & x = Intersect Y ) ) );