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 b1 being Element of the carrier of L st
( b1 in D & ( for b2 being Element of the carrier of L holds
( not b2 in D or not b1 <= b2 or b2 in U1 ) ) ) )

assume A2: sup D in U1 ; :: thesis: ex b1 being Element of the carrier of L st
( b1 in D & ( for b2 being Element of the carrier of L holds
( not b2 in D or not b1 <= b2 or b2 in U1 ) ) )

[(),(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 () such that
A3: for x being Element of () st y <= x holds
() . x in U1 by WAYBEL_0:def 11;
A4: y in the carrier of () ;
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 b1 being Element of the carrier of L holds
( not b1 in D or not y1 <= b1 or b1 in U1 ) ) )

thus y1 in D by ; :: thesis: for b1 being Element of the carrier of L holds
( not b1 in D or not y1 <= b1 or b1 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 () by ;
reconsider x = x as Element of () ;
() . x = the mapping of () . x by WAYBEL_0:def 8
.= (id D) . x by WAYBEL21:32
.= x by ;
hence x1 in U1 by ; :: thesis: verum