let L be non empty RelStr ; :: thesis: for N being non empty NetStr over L

for x being Element of L

for y being set holds

( y is Element of N iff y is Element of (x "/\" N) )

let N be non empty NetStr over L; :: thesis: for x being Element of L

for y being set holds

( y is Element of N iff y is Element of (x "/\" N) )

let x be Element of L; :: thesis: for y being set holds

( y is Element of N iff y is Element of (x "/\" N) )

let y be set ; :: thesis: ( y is Element of N iff y is Element of (x "/\" N) )

RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def3;

hence ( y is Element of N iff y is Element of (x "/\" N) ) ; :: thesis: verum

for x being Element of L

for y being set holds

( y is Element of N iff y is Element of (x "/\" N) )

let N be non empty NetStr over L; :: thesis: for x being Element of L

for y being set holds

( y is Element of N iff y is Element of (x "/\" N) )

let x be Element of L; :: thesis: for y being set holds

( y is Element of N iff y is Element of (x "/\" N) )

let y be set ; :: thesis: ( y is Element of N iff y is Element of (x "/\" N) )

RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def3;

hence ( y is Element of N iff y is Element of (x "/\" N) ) ; :: thesis: verum