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