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