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