let N be transitive RelStr ; for A, J being Subset of st A is_coarser_than uparrow J holds
uparrow A c= uparrow J
let A, J be Subset of ; ( 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 set ; 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 ;
consider t being Element of such that
A3:
t <= w1
and
A4:
t in A
by A2, WAYBEL_0:def 16;
consider t1 being Element of such that
A5:
t1 in uparrow J
and
A6:
t1 <= t
by A1, A4, YELLOW_4:def 2;
consider t2 being Element of such that
A7:
t2 <= t1
and
A8:
t2 in J
by A5, WAYBEL_0:def 16;
t2 <= t
by A6, A7, ORDERS_2:26;
then
t2 <= w1
by A3, ORDERS_2:26;
hence
w in uparrow J
by A8, WAYBEL_0:def 16; verum