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 that
A1: C is_coarser_than B and
A2: 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
A3: b in B and
A4: b <= c by A1;
consider a being Element of L such that
A5: ( a in A & a <= b ) by A2, A3;
take a ; :: thesis: ( a in A & a <= c )
thus ( a in A & a <= c ) by A4, A5, ORDERS_2:3; :: thesis: verum