let x be set ; :: thesis: for N being PT_net_Str st x is Element of the carrier of N & the carrier of N <> {} holds
x is Element of Elements N
let N be PT_net_Str ; :: thesis: ( x is Element of the carrier of N & the carrier of N <> {} implies x is Element of Elements N )
A1: the carrier of N c= Elements N by XBOOLE_1:7;
assume ( x is Element of the carrier of N & the carrier of N <> {} ) ; :: thesis: x is Element of Elements N
hence x is Element of Elements N by A1, TARSKI:def 3; :: thesis: verum