let L be transitive RelStr ; :: thesis: for A, B, C being Subset of L st C is_coarser_than B & B is_coarser_than A holds
C is_coarser_than A
let A, B, C be Subset of L; :: thesis: ( C is_coarser_than B & B is_coarser_than A implies C is_coarser_than A )
assume A1: ( C is_coarser_than B & B is_coarser_than A ) ; :: thesis: C is_coarser_than A
let c be Element of L; :: according to YELLOW_4:def 2 :: thesis: ( c in C implies ex a being Element of L st
( a in A & a <= c ) )
assume c in C ; :: thesis: ex a being Element of L st
( a in A & a <= c )
then consider b being Element of L such that
A2: ( b in B & b <= c ) by A1, Def2;
consider a being Element of L such that
A3: ( a in A & a <= b ) by A1, A2, Def2;
take a ; :: thesis: ( a in A & a <= c )
thus ( a in A & a <= c ) by A2, A3, ORDERS_2:26; :: thesis: verum