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