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