let N be transitive RelStr ; 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; ( A is_finer_than downarrow J implies downarrow A c= downarrow J )
assume A1:
A is_finer_than downarrow J
; downarrow A c= downarrow J
let w be object ; TARSKI:def 3 ( not w in downarrow A or w in downarrow J )
assume A2:
w in downarrow A
; w in downarrow J
then reconsider w1 = w as Element of N ;
consider t being Element of N such that
A3:
w1 <= t
and
A4:
t in A
by A2, WAYBEL_0:def 15;
consider t1 being Element of N such that
A5:
t1 in downarrow J
and
A6:
t <= t1
by A1, A4, YELLOW_4:def 1;
consider t2 being Element of N such that
A7:
t1 <= t2
and
A8:
t2 in J
by A5, WAYBEL_0:def 15;
w1 <= t1
by A3, A6, ORDERS_2:3;
then
w1 <= t2
by A7, ORDERS_2:3;
hence
w in downarrow J
by A8, WAYBEL_0:def 15; verum