assume 0 in X \ Y ; :: according to MEASURE6:def 7 :: thesis: contradiction
hence contradiction ; :: thesis: verum