let SFX, SFY be set ; :: thesis: ( SFX c= SFY implies SFX is_finer_than SFY )
assume A1: SFX c= SFY ; :: thesis: SFX is_finer_than SFY
let X be set ; :: according to SETFAM_1:def 2 :: thesis: ( X in SFX implies ex Y being set st
( Y in SFY & X c= Y ) )
assume A2: X in SFX ; :: thesis: ex Y being set st
( Y in SFY & X c= Y )
take X ; :: thesis: ( X in SFY & X c= X )
thus ( X in SFY & X c= X ) by A1, A2; :: thesis: verum