let L1, L2 be non empty 1-sorted ; 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; 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; ( 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
; for X being set st N1 is_eventually_in X holds
N2 is_eventually_in X
let X be set ; ( 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
; WAYBEL_0:def 11 N2 is_eventually_in X
reconsider i2 = i1 as Element of N2 by A1;
take
i2
; WAYBEL_0:def 11 for b1 being Element of the carrier of N2 holds
( not i2 <= b1 or N2 . b1 in X )
let j2 be Element of N2; ( not i2 <= j2 or N2 . j2 in X )
reconsider j1 = j2 as Element of N1 by A1;
assume
i2 <= j2
; N2 . j2 in X
then
N1 . j1 in X
by A1, A3, YELLOW_0:1;
hence
N2 . j2 in X
by A2; verum