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