let S be non empty reflexive antisymmetric RelStr ; :: thesis: for e being Element of S holds e = lim_inf (Net-Str e)
let e be Element of S; :: thesis: e = lim_inf (Net-Str e)
set N = Net-Str e;
set X = { ("/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S)) where j is Element of (Net-Str e) : verum } ;
reconsider e9 = e as Element of S ;
A1: { ("/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S)) where j is Element of (Net-Str e) : verum } c= {e9}
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { ("/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S)) where j is Element of (Net-Str e) : verum } or u in {e9} )
assume u in { ("/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S)) where j is Element of (Net-Str e) : verum } ; :: thesis: u in {e9}
then consider j being Element of (Net-Str e) such that
A2: u = "/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S) ;
set Y = { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ;
A3: { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } c= {e9}
proof
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } or v in {e9} )
assume v in { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ; :: thesis: v in {e9}
then consider i being Element of (Net-Str e) such that
A4: v = (Net-Str e) . i and
i >= j ;
reconsider i9 = i as Element of (Net-Str e) ;
(Net-Str e) . i9 = e by Th26;
hence v in {e9} by A4, TARSKI:def 1; :: thesis: verum
end;
reconsider j9 = j as Element of (Net-Str e) ;
j9 <= j9 ;
then (Net-Str e) . j in { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ;
then { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } = {e9} by A3, ZFMISC_1:33;
then u = e9 by A2, YELLOW_0:39;
hence u in {e9} by TARSKI:def 1; :: thesis: verum
end;
set j = the Element of (Net-Str e);
"/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= the Element of (Net-Str e) } ,S) in { ("/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S)) where j is Element of (Net-Str e) : verum } ;
then { ("/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S)) where j is Element of (Net-Str e) : verum } = {e9} by A1, ZFMISC_1:33;
hence e = lim_inf (Net-Str e) by YELLOW_0:39; :: thesis: verum