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:50;
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;