let L be non empty RelStr ; :: thesis: for V, S, T being Subset of L st S is_finer_than T & V is lower & T c= V holds
S c= V
let V, S, T be Subset of L; :: thesis: ( S is_finer_than T & V is lower & T c= V implies S c= V )
assume that
A1: S is_finer_than T and
A2: V is lower and
A3: T c= V ; :: thesis: S c= V
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in S or q in V )
assume A4: q in S ; :: thesis: q in V
then reconsider S1 = S as non empty Subset of L ;
reconsider a = q as Element of S1 by A4;
consider b being Element of L such that
A5: ( b in T & a <= b ) by A1, YELLOW_4:def 1;
thus q in V by A2, A3, A5, WAYBEL_0:def 19; :: thesis: verum