let SFX be set ; :: thesis: INTERSECTION (SFX,SFX) is_finer_than SFX

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

( Y in SFX & X c= Y ) )

assume X in INTERSECTION (SFX,SFX) ; :: thesis: ex Y being set st

( Y in SFX & X c= Y )

then consider Z1, Z2 being set such that

A1: Z1 in SFX and

Z2 in SFX and

A2: X = Z1 /\ Z2 by Def5;

take Z1 ; :: thesis: ( Z1 in SFX & X c= Z1 )

thus ( Z1 in SFX & X c= Z1 ) by A1, A2, XBOOLE_1:17; :: thesis: verum

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

( Y in SFX & X c= Y ) )

assume X in INTERSECTION (SFX,SFX) ; :: thesis: ex Y being set st

( Y in SFX & X c= Y )

then consider Z1, Z2 being set such that

A1: Z1 in SFX and

Z2 in SFX and

A2: X = Z1 /\ Z2 by Def5;

take Z1 ; :: thesis: ( Z1 in SFX & X c= Z1 )

thus ( Z1 in SFX & X c= Z1 ) by A1, A2, XBOOLE_1:17; :: thesis: verum