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