assume 0 in X \ Y ; :: according to PSCOMP_1:def 1 :: thesis: contradiction
hence contradiction ; :: thesis: verum