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₁ being Element of the carrier of N st
( b₁ in D & ( for b₂ being Element of the carrier of N holds
( not b₂ in D or not b₁ <= b₂ or b₂ in uparrow A ) ) ) )
assume sup D in uparrow A ; :: thesis: ex b₁ being Element of the carrier of N st
( b₁ in D & ( for b₂ being Element of the carrier of N holds
( not b₂ in D or not b₁ <= b₂ or b₂ in uparrow A ) ) )
then consider a being Element of N such that
A2: ( a <= sup D & 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
A3: ( y in aa "/\" D & ( for x being Element of N st x in aa "/\" D & x >= y holds
x in A ) ) by A1, A2;
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
A4: ( y = a "/\" d & d in D ) by A3;
take d ; :: thesis: ( d in D & ( for b₁ being Element of the carrier of N holds
( not b₁ in D or not d <= b₁ or b₁ in uparrow A ) ) )
thus d in D by A4; :: thesis: for b₁ being Element of the carrier of N holds
( not b₁ in D or not d <= b₁ or b₁ in uparrow A )
let x be Element of N; :: thesis: ( not x in D or not d <= x or x in uparrow A )
assume A5: ( x in D & x >= d ) ; :: thesis: x in uparrow A
A6: y in A by A3, ORDERS_2:24;
d >= y by A4, YELLOW_0:23;
then x >= y by A5, ORDERS_2:26;
hence x in uparrow A by A6, WAYBEL_0:def 16; :: thesis: verum