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:
let D be non empty directed Subset of N; :: according to WAYBEL11:def 3 :: thesis: ( not "\/" (D,N) in uparrow A or ex b1 being Element of the carrier of N st
( b1 in D & ( for b2 being Element of the carrier of N holds
( not b2 in D or not b1 <= b2 or b2 in uparrow A ) ) ) )

assume sup D in uparrow A ; :: thesis: ex b1 being Element of the carrier of N st
( b1 in D & ( for b2 being Element of the carrier of N holds
( not b2 in D or not b1 <= b2 or b2 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 ;
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 b1 being Element of the carrier of N holds
( not b1 in D or not d <= b1 or b1 in uparrow A ) ) )

thus d in D by A7; :: thesis: for b1 being Element of the carrier of N holds
( not b1 in D or not d <= b1 or b1 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:
d >= y by ;
then A9: x >= y by ;
y in A by ;
hence x in uparrow A by ; :: thesis: verum