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_{1} being Element of the carrier of L st

( b_{1} in D & ( for b_{2} being Element of the carrier of L holds

( not b_{2} in D or not b_{1} <= b_{2} or b_{2} in U1 ) ) ) )

assume A2: sup D in U1 ; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} in D & ( for b_{2} being Element of the carrier of L holds

( not b_{2} in D or not b_{1} <= b_{2} or b_{2} 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_{1} being Element of the carrier of L holds

( not b_{1} in D or not y1 <= b_{1} or b_{1} in U1 ) ) )

thus y1 in D by A4, WAYBEL21:32; :: thesis: for b_{1} being Element of the carrier of L holds

( not b_{1} in D or not y1 <= b_{1} or b_{1} 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

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

( b

( not b

assume A2: sup D in U1 ; :: thesis: ex b

( b

( not b

[(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

( not b

thus y1 in D by A4, WAYBEL21:32; :: thesis: for b

( not b

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