let SFX, SFY, SFZ be set ; :: thesis: ( SFX is_finer_than SFY & SFY is_finer_than SFZ implies SFX is_finer_than SFZ )

assume that

A1: for X being set st X in SFX holds

ex Y being set st

( Y in SFY & X c= Y ) and

A2: for X being set st X in SFY holds

ex Y being set st

( Y in SFZ & X c= Y ) ; :: according to SETFAM_1:def 2 :: thesis: SFX is_finer_than SFZ

let X be set ; :: according to SETFAM_1:def 2 :: thesis: ( X in SFX implies ex Y being set st

( Y in SFZ & X c= Y ) )

assume X in SFX ; :: thesis: ex Y being set st

( Y in SFZ & X c= Y )

then consider Y being set such that

A3: Y in SFY and

A4: X c= Y by A1;

consider Z being set such that

A5: ( Z in SFZ & Y c= Z ) by A2, A3;

take Z ; :: thesis: ( Z in SFZ & X c= Z )

thus ( Z in SFZ & X c= Z ) by A4, A5; :: thesis: verum

assume that

A1: for X being set st X in SFX holds

ex Y being set st

( Y in SFY & X c= Y ) and

A2: for X being set st X in SFY holds

ex Y being set st

( Y in SFZ & X c= Y ) ; :: according to SETFAM_1:def 2 :: thesis: SFX is_finer_than SFZ

let X be set ; :: according to SETFAM_1:def 2 :: thesis: ( X in SFX implies ex Y being set st

( Y in SFZ & X c= Y ) )

assume X in SFX ; :: thesis: ex Y being set st

( Y in SFZ & X c= Y )

then consider Y being set such that

A3: Y in SFY and

A4: X c= Y by A1;

consider Z being set such that

A5: ( Z in SFZ & Y c= Z ) by A2, A3;

take Z ; :: thesis: ( Z in SFZ & X c= Z )

thus ( Z in SFZ & X c= Z ) by A4, A5; :: thesis: verum