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