let X, Y, SFX be set ; :: thesis: ( SFX is_finer_than {X,Y} implies for Z being set holds

( not Z in SFX or Z c= X or Z c= Y ) )

assume A1: for Z1 being set st Z1 in SFX holds

ex Z2 being set st

( Z2 in {X,Y} & Z1 c= Z2 ) ; :: according to SETFAM_1:def 2 :: thesis: for Z being set holds

( not Z in SFX or Z c= X or Z c= Y )

let Z be set ; :: thesis: ( not Z in SFX or Z c= X or Z c= Y )

assume Z in SFX ; :: thesis: ( Z c= X or Z c= Y )

then consider Z2 being set such that

A2: Z2 in {X,Y} and

A3: Z c= Z2 by A1;

{X,Y} = {X} \/ {Y} by ENUMSET1:1;

then ( Z2 in {X} or Z2 in {Y} ) by A2, XBOOLE_0:def 3;

hence ( Z c= X or Z c= Y ) by A3, TARSKI:def 1; :: thesis: verum

( not Z in SFX or Z c= X or Z c= Y ) )

assume A1: for Z1 being set st Z1 in SFX holds

ex Z2 being set st

( Z2 in {X,Y} & Z1 c= Z2 ) ; :: according to SETFAM_1:def 2 :: thesis: for Z being set holds

( not Z in SFX or Z c= X or Z c= Y )

let Z be set ; :: thesis: ( not Z in SFX or Z c= X or Z c= Y )

assume Z in SFX ; :: thesis: ( Z c= X or Z c= Y )

then consider Z2 being set such that

A2: Z2 in {X,Y} and

A3: Z c= Z2 by A1;

{X,Y} = {X} \/ {Y} by ENUMSET1:1;

then ( Z2 in {X} or Z2 in {Y} ) by A2, XBOOLE_0:def 3;

hence ( Z c= X or Z c= Y ) by A3, TARSKI:def 1; :: thesis: verum