let L be non empty RelStr ; :: thesis: for N being non empty NetStr of 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 of 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