let X, Y be set ; :: thesis: INTERSECTION (X,Y) is_finer_than X

now :: thesis: for xy being set st xy in INTERSECTION (X,Y) holds
ex x being set st
( x in X & xy c= x )

let xy be set ; :: thesis: ( xy in INTERSECTION (X,Y) implies ex x being set st
( x in X & xy c= x ) )
assume xy in INTERSECTION (X,Y) ; :: thesis: ex x being set st
( x in X & xy c= x )
then consider x, y being set such that
A1: ( x in X & y in Y & xy = x /\ y ) by SETFAM_1:def 5;
take x = x; :: thesis: ( x in X & xy c= x )
thus ( x in X & xy c= x ) by A1; :: thesis: verum

end;

hence INTERSECTION (X,Y) is_finer_than X by SETFAM_1:def 2; :: thesis: verum