let L be complete LATTICE; :: thesis: for U1 being Subset of L st U1 in xi L holds
U1 is property(S)
let U1 be Subset of L; :: thesis: ( U1 in xi L implies U1 is property(S) )
assume U1 in xi L ; :: thesis: U1 is property(S)
then U1 in { V where V is Subset of L : for p being Element of L st p in V holds
for N being net of L st [N,p] in lim_inf-Convergence L holds
N is_eventually_in V } by YELLOW_6:def 24;
then A1: ex V being Subset of L st
( U1 = V & ( for p being Element of L st p in V holds
for N being net of L st [N,p] in lim_inf-Convergence L holds
N is_eventually_in V ) ) ;
let D be non empty directed Subset of L; :: according to WAYBEL11:def 3 :: thesis: ( not "\/" (D,L) in U1 or ex b₁ being Element of the carrier of L st
( b₁ in D & ( for b₂ being Element of the carrier of L holds
( not b₂ in D or not b₁ <= b₂ or b₂ in U1 ) ) ) )
assume A2: sup D in U1 ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in D & ( for b₂ being Element of the carrier of L holds
( not b₂ in D or not b₁ <= b₂ or b₂ in U1 ) ) )
[(Net-Str D),(sup D)] in lim_inf-Convergence L by Th26;
then Net-Str D is_eventually_in U1 by A1, A2;
then consider y being Element of (Net-Str D) such that
A3: for x being Element of (Net-Str D) st y <= x holds
(Net-Str D) . x in U1 by WAYBEL_0:def 11;
A4: y in the carrier of (Net-Str D) ;
then y in D by WAYBEL21:32;
then reconsider y1 = y as Element of L ;
reconsider y1 = y1 as Element of L ;
take y1 ; :: thesis: ( y1 in D & ( for b₁ being Element of the carrier of L holds
( not b₁ in D or not y1 <= b₁ or b₁ in U1 ) ) )
thus y1 in D by A4, WAYBEL21:32; :: thesis: for b₁ being Element of the carrier of L holds
( not b₁ in D or not y1 <= b₁ or b₁ in U1 )
let x1 be Element of L; :: thesis: ( not x1 in D or not y1 <= x1 or x1 in U1 )
assume that
A5: x1 in D and
A6: x1 >= y1 ; :: thesis: x1 in U1
A7: Net-Str D is full SubRelStr of L by WAYBEL21:32;
reconsider x = x1 as Element of (Net-Str D) by A5, WAYBEL21:32;
reconsider x = x as Element of (Net-Str D) ;
(Net-Str D) . x = the mapping of (Net-Str D) . x by WAYBEL_0:def 8
.= (id D) . x by WAYBEL21:32
.= x by A5, FUNCT_1:18 ;
hence x1 in U1 by A3, A6, A7, YELLOW_0:60; :: thesis: verum