let x be set ; :: thesis: for N being Pnet

for y being Element of Elements N st y in the carrier' of N holds

( x in Pre (N,y) iff pre N,y,x )

let N be Pnet; :: thesis: for y being Element of Elements N st y in the carrier' of N holds

( x in Pre (N,y) iff pre N,y,x )

let y be Element of Elements N; :: thesis: ( y in the carrier' of N implies ( x in Pre (N,y) iff pre N,y,x ) )

assume A1: y in the carrier' of N ; :: thesis: ( x in Pre (N,y) iff pre N,y,x )

A2: ( pre N,y,x implies x in Pre (N,y) )

hence ( x in Pre (N,y) iff pre N,y,x ) by A2; :: thesis: verum

for y being Element of Elements N st y in the carrier' of N holds

( x in Pre (N,y) iff pre N,y,x )

let N be Pnet; :: thesis: for y being Element of Elements N st y in the carrier' of N holds

( x in Pre (N,y) iff pre N,y,x )

let y be Element of Elements N; :: thesis: ( y in the carrier' of N implies ( x in Pre (N,y) iff pre N,y,x ) )

assume A1: y in the carrier' of N ; :: thesis: ( x in Pre (N,y) iff pre N,y,x )

A2: ( pre N,y,x implies x in Pre (N,y) )

proof

( x in Pre (N,y) implies pre N,y,x )
by Def6, A1;
assume
pre N,y,x
; :: thesis: x in Pre (N,y)

then A3: [x,y] in Flow N ;

then x in the carrier of N by A1, Th6;

then x in Elements N by XBOOLE_0:def 3;

hence x in Pre (N,y) by A3, Def6; :: thesis: verum

end;then A3: [x,y] in Flow N ;

then x in the carrier of N by A1, Th6;

then x in Elements N by XBOOLE_0:def 3;

hence x in Pre (N,y) by A3, Def6; :: thesis: verum

hence ( x in Pre (N,y) iff pre N,y,x ) by A2; :: thesis: verum