let X, Y be set ; :: thesis: ( ( for y being object holds

( y in X iff ( y in the carrier of N & [x,y] in Flow N ) ) ) & ( for y being object holds

( y in Y iff ( y in the carrier of N & [x,y] in Flow N ) ) ) implies X = Y )

assume that

A4: for y being object holds

( y in X iff ( y in the carrier of N & [x,y] in Flow N ) ) and

A5: for y being object holds

( y in Y iff ( y in the carrier of N & [x,y] in Flow N ) ) ; :: thesis: X = Y

A6: for y being object st y in Y holds

y in X

y in Y

( y in X iff ( y in the carrier of N & [x,y] in Flow N ) ) ) & ( for y being object holds

( y in Y iff ( y in the carrier of N & [x,y] in Flow N ) ) ) implies X = Y )

assume that

A4: for y being object holds

( y in X iff ( y in the carrier of N & [x,y] in Flow N ) ) and

A5: for y being object holds

( y in Y iff ( y in the carrier of N & [x,y] in Flow N ) ) ; :: thesis: X = Y

A6: for y being object st y in Y holds

y in X

proof

for y being object st y in X holds
let y be object ; :: thesis: ( y in Y implies y in X )

assume y in Y ; :: thesis: y in X

then ( y in the carrier of N & [x,y] in Flow N ) by A5;

hence y in X by A4; :: thesis: verum

end;assume y in Y ; :: thesis: y in X

then ( y in the carrier of N & [x,y] in Flow N ) by A5;

hence y in X by A4; :: thesis: verum

y in Y

proof

hence
X = Y
by A6, TARSKI:2; :: thesis: verum
let y be object ; :: thesis: ( y in X implies y in Y )

assume y in X ; :: thesis: y in Y

then ( y in the carrier of N & [x,y] in Flow N ) by A4;

hence y in Y by A5; :: thesis: verum

end;assume y in X ; :: thesis: y in Y

then ( y in the carrier of N & [x,y] in Flow N ) by A4;

hence y in Y by A5; :: thesis: verum