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