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;