per cases ( not n in dom X or n in dom X ) ;

suppose not n in dom X ; :: thesis: X . n is Subset of

then X . n = {} by FUNCT_1:def 4;
hence X . n is Subset of by XBOOLE_1:2; :: thesis: verum

end;

suppose n in dom X ; :: thesis: X . n is Subset of

hence X . n is Subset of by FINSEQ_2:13; :: thesis: verum

end;

end;