let S be non empty 1-sorted ; :: thesis: for e being Element of S
for X being set holds
( Net-Str e is_eventually_in X iff e in X )
let e be Element of S; :: thesis: for X being set holds
( Net-Str e is_eventually_in X iff e in X )
let X be set ; :: thesis: ( Net-Str e is_eventually_in X iff e in X )
set N = Net-Str e;
the carrier of (Net-Str e) = {e} by Def11;
then reconsider d = e as Element of (Net-Str e) by TARSKI:def 1;
hereby :: thesis: ( e in X implies Net-Str e is_eventually_in X )
assume Net-Str e is_eventually_in X ; :: thesis: e in X
then consider x being Element of (Net-Str e) such that
A1: for y being Element of (Net-Str e) st x <= y holds
(Net-Str e) . y in X ;
(Net-Str e) . x in X by A1;
hence e in X by Th26; :: thesis: verum
end;
assume A2: e in X ; :: thesis: Net-Str e is_eventually_in X
take d ; :: according to WAYBEL_0:def 11 :: thesis: for b1 being Element of the carrier of (Net-Str e) holds
( not d <= b1 or (Net-Str e) . b1 in X )
let j be Element of (Net-Str e); :: thesis: ( not d <= j or (Net-Str e) . j in X )
assume d <= j ; :: thesis: (Net-Str e) . j in X
thus (Net-Str e) . j in X by A2, Th26; :: thesis: verum