let N be transitive RelStr ; :: thesis: for A, J being Subset of N st A is_coarser_than uparrow J holds
uparrow A c= uparrow J
let A, J be Subset of N; :: thesis: ( A is_coarser_than uparrow J implies uparrow A c= uparrow J )
assume A1: A is_coarser_than uparrow J ; :: thesis: uparrow A c= uparrow J
let w be set ; :: according to TARSKI:def 3 :: thesis: ( not w in uparrow A or w in uparrow J )
assume A2: w in uparrow A ; :: thesis: w in uparrow J
then reconsider w1 = w as Element of N ;
consider t being Element of N such that
A3: ( t <= w1 & t in A ) by A2, WAYBEL_0:def 16;
consider t1 being Element of N such that
A4: ( t1 in uparrow J & t1 <= t ) by A1, A3, YELLOW_4:def 2;
consider t2 being Element of N such that
A5: ( t2 <= t1 & t2 in J ) by A4, WAYBEL_0:def 16;
t2 <= t by A4, A5, ORDERS_2:26;
then t2 <= w1 by A3, ORDERS_2:26;
hence w in uparrow J by A5, WAYBEL_0:def 16; :: thesis: verum