reconsider E = {} R^1 as Subset of R^1 ;
assume {} in Kurat14Set KurExSet ; :: according to SETFAM_1:def 9 :: thesis: contradiction
then E ` in Kurat14Set KurExSet by Th6;
hence contradiction by SETFAM_1:def 13; :: thesis: verum