less_dom f,a c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in less_dom f,a or x in X )
assume x in less_dom f,a ; :: thesis: x in X
then A1: x in dom f by Def12;
dom f c= X by RELAT_1:def 18;
hence x in X by A1; :: thesis: verum

end;

hence less_dom f,a is Subset of X ; :: thesis: verum