let n be non empty Nat; :: thesis: for x being set holds
( not x in n or x = 0 or ( x in Seg n & x <> n ) )
let x be set ; :: thesis: ( not x in n or x = 0 or ( x in Seg n & x <> n ) )
assume x in n ; :: thesis: ( x = 0 or ( x in Seg n & x <> n ) )
then x in {0} \/ ((Seg n) \ {n}) by th1;
then ( x in {0} or x in (Seg n) \ {n} ) by XBOOLE_0:def 3;
then ( x = 0 or ( x in Seg n & not x in {n} ) ) by TARSKI:def 1, XBOOLE_0:def 5;
hence ( x = 0 or ( x in Seg n & x <> n ) ) by TARSKI:def 1; :: thesis: verum