let L be RelStr ; :: thesis: for A, B being Subset of L st B is_finer_than A & A is lower holds
B c= A
let A, B be Subset of L; :: thesis: ( B is_finer_than A & A is lower implies B c= A )
assume that
A1: B is_finer_than A and
A2: A is lower ; :: thesis: B c= A
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in B or a in A )
assume A3: a in B ; :: thesis: a in A
then reconsider a1 = a as Element of L ;
ex b being Element of L st
( b in A & a1 <= b ) by A1, A3;
hence a in A by A2; :: thesis: verum