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 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₁ 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 A7; :: 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 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