theorem Th3: :: RANKNULL:3
for V being 1-sorted
for X, Y being Subset of V holds
( X meets Y iff ex v being Element of V st
( v in X & v in Y ) )