set A = KurExSet ;
assume {(Int KurExSet ),(Int (Cl KurExSet )),(Int (Cl (Int KurExSet ))),(Cl KurExSet ),(Cl (Int KurExSet )),(Cl (Int (Cl KurExSet )))} meets {KurExSet } ; :: thesis: contradiction
then A1: KurExSet in {(Int KurExSet ),(Int (Cl KurExSet )),(Int (Cl (Int KurExSet ))),(Cl KurExSet ),(Cl (Int KurExSet )),(Cl (Int (Cl KurExSet )))} by ZFMISC_1:56;

per cases ( KurExSet = Int KurExSet or KurExSet = Int (Cl KurExSet ) or KurExSet = Int (Cl (Int KurExSet )) or KurExSet = Cl KurExSet or KurExSet = Cl (Int KurExSet ) or KurExSet = Cl (Int (Cl KurExSet )) ) by A1, ENUMSET1:def 4;

suppose KurExSet = Int KurExSet ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

suppose KurExSet = Int (Cl KurExSet ) ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

suppose KurExSet = Int (Cl (Int KurExSet )) ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

suppose KurExSet = Cl KurExSet ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

suppose KurExSet = Cl (Int KurExSet ) ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

suppose KurExSet = Cl (Int (Cl KurExSet )) ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

end;