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_{1} being set st

( b_{1} in C & b_{1} c= a ) )

assume a in A ; :: thesis: ex b_{1} being set st

( b_{1} in C & b_{1} 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

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

( b

assume a in A ; :: thesis: ex b

( b

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