set A = KurExSet ;
assume A2: the carrier of R^1 in Kurat14OpPart KurExSet ; :: according to SETFAM_1:def 12 :: thesis: contradiction
per cases ( REAL = (Cl KurExSet) ` or REAL = (Cl ((Cl KurExSet) `)) ` or REAL = (Cl ((Cl ((Cl KurExSet) `)) `)) ` or REAL = (Cl (KurExSet `)) ` or REAL = (Cl ((Cl (KurExSet `)) `)) ` or REAL = (Cl ((Cl ((Cl (KurExSet `)) `)) `)) ` ) by A2, ENUMSET1:def 4, TOPMETR:17;
suppose REAL = (Cl KurExSet) ` ; :: thesis: contradiction
hence contradiction by Th10, BORSUK_5:72; :: thesis: verum
end;
suppose REAL = (Cl ((Cl KurExSet) `)) ` ; :: thesis: contradiction
hence contradiction by Th12, BORSUK_5:72; :: thesis: verum
end;
suppose REAL = (Cl ((Cl ((Cl KurExSet) `)) `)) ` ; :: thesis: contradiction
hence contradiction by Th14, BORSUK_5:72; :: thesis: verum
end;
suppose REAL = (Cl (KurExSet `)) ` ; :: thesis: contradiction
hence contradiction by Th17, BORSUK_5:72; :: thesis: verum
end;
suppose REAL = (Cl ((Cl (KurExSet `)) `)) ` ; :: thesis: contradiction
hence contradiction by Th19, BORSUK_5:72; :: thesis: verum
end;
suppose REAL = (Cl ((Cl ((Cl (KurExSet `)) `)) `)) ` ; :: thesis: contradiction
hence contradiction by Th21, BORSUK_5:72; :: thesis: verum
end;
end;