let n be Nat; :: thesis: for t, z being Integer st n > 0 & not t divides (t + z) |^ n holds
not t divides z
let t, z be Integer; :: thesis: ( n > 0 & not t divides (t + z) |^ n implies not t divides z )
assume ( n > 0 & not t divides (t + z) |^ n ) ; :: thesis: not t divides z
then not t divides t + z by Th14;
hence not t divides z by WSIERP_1:4; :: thesis: verum