let L be non empty transitive RelStr ; :: thesis: for A, B being Subset of L st A is_coarser_than B holds
uparrow A c= uparrow B
let A, B be Subset of L; :: thesis: ( A is_coarser_than B implies uparrow A c= uparrow B )
assume A1: for a being Element of L st a in A holds
ex b being Element of L st
( b in B & b <= a ) ; :: according to YELLOW_4:def 2 :: thesis: uparrow A c= uparrow B
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in uparrow A or q in uparrow B )
assume A2: q in uparrow A ; :: thesis: q in uparrow B
then reconsider q1 = q as Element of L ;
consider a being Element of L such that
A3: a <= q1 and
A4: a in A by A2, WAYBEL_0:def 16;
consider b being Element of L such that
A5: b in B and
A6: b <= a by A1, A4;
b <= q1 by A3, A6, ORDERS_2:3;
hence q in uparrow B by A5, WAYBEL_0:def 16; :: thesis: verum