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₁ being Element of the carrier of N2 holds
( not i2 <= b₁ or N2 . b₁ 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