let L be non empty transitive RelStr ; :: thesis: for A, B being Subset of L st A is_finer_than B holds

downarrow A c= downarrow B

let A, B be Subset of L; :: thesis: ( A is_finer_than B implies downarrow A c= downarrow 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 1 :: thesis: downarrow A c= downarrow B

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in downarrow A or q in downarrow B )

assume A2: q in downarrow A ; :: thesis: q in downarrow 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 15;

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 downarrow B by A5, WAYBEL_0:def 15; :: thesis: verum

downarrow A c= downarrow B

let A, B be Subset of L; :: thesis: ( A is_finer_than B implies downarrow A c= downarrow 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 1 :: thesis: downarrow A c= downarrow B

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in downarrow A or q in downarrow B )

assume A2: q in downarrow A ; :: thesis: q in downarrow 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 15;

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 downarrow B by A5, WAYBEL_0:def 15; :: thesis: verum