let N be meet-continuous LATTICE; :: thesis: for A being Subset of N st A is property(S) holds

uparrow A is property(S)

let A be Subset of N; :: thesis: ( A is property(S) implies uparrow A is property(S) )

assume A1: for D being non empty directed Subset of N st sup D in A holds

ex y being Element of N st

( y in D & ( for x being Element of N st x in D & x >= y holds

x in A ) ) ; :: according to WAYBEL11:def 3 :: thesis: uparrow A is property(S)

let D be non empty directed Subset of N; :: according to WAYBEL11:def 3 :: thesis: ( not "\/" (D,N) in uparrow A or ex b_{1} being Element of the carrier of N st

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

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

assume sup D in uparrow A ; :: thesis: ex b_{1} being Element of the carrier of N st

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

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

then consider a being Element of N such that

A2: a <= sup D and

A3: a in A by WAYBEL_0:def 16;

reconsider aa = {a} as non empty directed Subset of N by WAYBEL_0:5;

a = sup ({a} "/\" D) by A2, WAYBEL_2:52;

then consider y being Element of N such that

A4: y in aa "/\" D and

A5: for x being Element of N st x in aa "/\" D & x >= y holds

x in A by A1, A3;

aa "/\" D = { (a "/\" d) where d is Element of N : d in D } by YELLOW_4:42;

then consider d being Element of N such that

A6: y = a "/\" d and

A7: d in D by A4;

take d ; :: thesis: ( d in D & ( for b_{1} being Element of the carrier of N holds

( not b_{1} in D or not d <= b_{1} or b_{1} in uparrow A ) ) )

thus d in D by A7; :: thesis: for b_{1} being Element of the carrier of N holds

( not b_{1} in D or not d <= b_{1} or b_{1} in uparrow A )

let x be Element of N; :: thesis: ( not x in D or not d <= x or x in uparrow A )

assume that

x in D and

A8: x >= d ; :: thesis: x in uparrow A

d >= y by A6, YELLOW_0:23;

then A9: x >= y by A8, ORDERS_2:3;

y in A by A4, A5, ORDERS_2:1;

hence x in uparrow A by A9, WAYBEL_0:def 16; :: thesis: verum

uparrow A is property(S)

let A be Subset of N; :: thesis: ( A is property(S) implies uparrow A is property(S) )

assume A1: for D being non empty directed Subset of N st sup D in A holds

ex y being Element of N st

( y in D & ( for x being Element of N st x in D & x >= y holds

x in A ) ) ; :: according to WAYBEL11:def 3 :: thesis: uparrow A is property(S)

let D be non empty directed Subset of N; :: according to WAYBEL11:def 3 :: thesis: ( not "\/" (D,N) in uparrow A or ex b

( b

( not b

assume sup D in uparrow A ; :: thesis: ex b

( b

( not b

then consider a being Element of N such that

A2: a <= sup D and

A3: a in A by WAYBEL_0:def 16;

reconsider aa = {a} as non empty directed Subset of N by WAYBEL_0:5;

a = sup ({a} "/\" D) by A2, WAYBEL_2:52;

then consider y being Element of N such that

A4: y in aa "/\" D and

A5: for x being Element of N st x in aa "/\" D & x >= y holds

x in A by A1, A3;

aa "/\" D = { (a "/\" d) where d is Element of N : d in D } by YELLOW_4:42;

then consider d being Element of N such that

A6: y = a "/\" d and

A7: d in D by A4;

take d ; :: thesis: ( d in D & ( for b

( not b

thus d in D by A7; :: thesis: for b

( not b

let x be Element of N; :: thesis: ( not x in D or not d <= x or x in uparrow A )

assume that

x in D and

A8: x >= d ; :: thesis: x in uparrow A

d >= y by A6, YELLOW_0:23;

then A9: x >= y by A8, ORDERS_2:3;

y in A by A4, A5, ORDERS_2:1;

hence x in uparrow A by A9, WAYBEL_0:def 16; :: thesis: verum