assume A ` is empty ; :: thesis: contradiction
then (A `) ` = X ;
hence contradiction by SUBSET_1:def 6; :: thesis: verum