per cases ( SF is empty or not SF is empty ) ;

suppose SF is empty ; :: thesis: [:(X \ A),(X \ A):] \/ [:A,A:] is Subset of [:X,X:]

then A is empty by SUBSET_1:def 1;
then [:A,A:] c= [:X,X:] ;
hence [:(X \ A),(X \ A):] \/ [:A,A:] is Subset of [:X,X:] by XBOOLE_1:8; :: thesis: verum

end;

suppose not SF is empty ; :: thesis: [:(X \ A),(X \ A):] \/ [:A,A:] is Subset of [:X,X:]

then A in SF ;
then [:A,A:] c= [:X,X:] by ZFMISC_1:96;
hence [:(X \ A),(X \ A):] \/ [:A,A:] is Subset of [:X,X:] by XBOOLE_1:8; :: thesis: verum

end;

end;