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 & T c= V ) ; :: thesis: S c= V
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in S or q in V )
assume A3: 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 A3;
ex b being Element of L st
( b in T & a <= b ) by A1;
hence q in V by A2; :: thesis: verum