let L be non empty RelStr ; :: thesis: for N being non empty NetStr of L
for x being Element of
for y being set holds
( y is Element of iff y is Element of )
let N be non empty NetStr of L; :: thesis: for x being Element of
for y being set holds
( y is Element of iff y is Element of )
let x be Element of ; :: thesis: for y being set holds
( y is Element of iff y is Element of )
let y be set ; :: thesis: ( y is Element of iff y is Element of )
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 iff y is Element of ) ; :: thesis: verum