let L1, L2 be non empty 1-sorted ; :: thesis: for N1 being non empty NetStr over L1

for N2 being non empty NetStr over L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds

for X being set st N1 is_eventually_in X holds

N2 is_eventually_in X

let N1 be non empty NetStr over L1; :: thesis: for N2 being non empty NetStr over L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds

for X being set st N1 is_eventually_in X holds

N2 is_eventually_in X

let N2 be non empty NetStr over L2; :: thesis: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 implies for X being set st N1 is_eventually_in X holds

N2 is_eventually_in X )

assume that

A1: RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) and

A2: the mapping of N1 = the mapping of N2 ; :: thesis: for X being set st N1 is_eventually_in X holds

N2 is_eventually_in X

let X be set ; :: thesis: ( N1 is_eventually_in X implies N2 is_eventually_in X )

given i1 being Element of N1 such that A3: for j being Element of N1 st i1 <= j holds

N1 . j in X ; :: according to WAYBEL_0:def 11 :: thesis: N2 is_eventually_in X

reconsider i2 = i1 as Element of N2 by A1;

take i2 ; :: according to WAYBEL_0:def 11 :: thesis: for b_{1} being Element of the carrier of N2 holds

( not i2 <= b_{1} or N2 . b_{1} in X )

let j2 be Element of N2; :: thesis: ( not i2 <= j2 or N2 . j2 in X )

reconsider j1 = j2 as Element of N1 by A1;

assume i2 <= j2 ; :: thesis: N2 . j2 in X

then N1 . j1 in X by A1, A3, YELLOW_0:1;

hence N2 . j2 in X by A2; :: thesis: verum

for N2 being non empty NetStr over L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds

for X being set st N1 is_eventually_in X holds

N2 is_eventually_in X

let N1 be non empty NetStr over L1; :: thesis: for N2 being non empty NetStr over L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds

for X being set st N1 is_eventually_in X holds

N2 is_eventually_in X

let N2 be non empty NetStr over L2; :: thesis: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 implies for X being set st N1 is_eventually_in X holds

N2 is_eventually_in X )

assume that

A1: RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) and

A2: the mapping of N1 = the mapping of N2 ; :: thesis: for X being set st N1 is_eventually_in X holds

N2 is_eventually_in X

let X be set ; :: thesis: ( N1 is_eventually_in X implies N2 is_eventually_in X )

given i1 being Element of N1 such that A3: for j being Element of N1 st i1 <= j holds

N1 . j in X ; :: according to WAYBEL_0:def 11 :: thesis: N2 is_eventually_in X

reconsider i2 = i1 as Element of N2 by A1;

take i2 ; :: according to WAYBEL_0:def 11 :: thesis: for b

( not i2 <= b

let j2 be Element of N2; :: thesis: ( not i2 <= j2 or N2 . j2 in X )

reconsider j1 = j2 as Element of N1 by A1;

assume i2 <= j2 ; :: thesis: N2 . j2 in X

then N1 . j1 in X by A1, A3, YELLOW_0:1;

hence N2 . j2 in X by A2; :: thesis: verum