let T1, T2 be non empty 1-sorted ; :: thesis: for X being set
for N1 being net of T1
for N2 being net of T2 st N1 = N2 & N1 is_eventually_in X holds
N2 is_eventually_in X
let X be set ; :: thesis: for N1 being net of T1
for N2 being net of T2 st N1 = N2 & N1 is_eventually_in X holds
N2 is_eventually_in X
let N1 be net of T1; :: thesis: for N2 being net of T2 st N1 = N2 & N1 is_eventually_in X holds
N2 is_eventually_in X
let N2 be net of T2; :: thesis: ( N1 = N2 & N1 is_eventually_in X implies N2 is_eventually_in X )
assume A1: N1 = N2 ; :: thesis: ( not N1 is_eventually_in X or N2 is_eventually_in X )
assume N1 is_eventually_in X ; :: thesis: N2 is_eventually_in X
then consider i being Element of N1 such that
A2: for j being Element of N1 st i <= j holds
N1 . j in X ;
reconsider ii = i as Element of N2 by A1;
take ii ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of N2 holds
( not ii <= b₁ or N2 . b₁ in X )
let jj be Element of N2; :: thesis: ( not ii <= jj or N2 . jj in X )
reconsider j = jj as Element of N1 by A1;
assume A3: ii <= jj ; :: thesis: N2 . jj in X
N2 . jj = N1 . j by A1;
hence N2 . jj in X by A1, A2, A3; :: thesis: verum