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

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