for X, Y being set
for A being Subset-Family of X
for B being Subset-Family of Y st A = B & X in A holds
FinMeetCl B = {Y} \/ (FinMeetCl A)