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

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