for n being Nat
for X being set
for Fx being Subset-Family of X st order Fx <= n holds
for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds
meet Gx is empty