let A, B, C be set ; :: thesis: ( A is_coarser_than B & B is_coarser_than C implies A is_coarser_than C )
assume that
A1: A is_coarser_than B and
A2: B is_coarser_than C ; :: thesis: A is_coarser_than C
let a be set ; :: according to SETFAM_1:def 3 :: thesis: ( not a in A or ex b₁ being set st
( b₁ in C & b₁ c= a ) )
assume a in A ; :: thesis: ex b₁ being set st
( b₁ in C & b₁ c= a )
then consider b being set such that
A3: b in B and
A4: b c= a by A1;
consider c being set such that
A5: ( c in C & c c= b ) by A2, A3;
take c ; :: thesis: ( c in C & c c= a )
thus ( c in C & c c= a ) by A4, A5; :: thesis: verum