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