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