A13: great_eq_dom f,a c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in great_eq_dom f,a or x in X )
assume A14: x in great_eq_dom f,a ; :: thesis: x in X
A15: x in dom f by A14, Def15;
A16: dom f c= X by RELAT_1:def 18;
thus x in X by A15, A16; :: thesis: verum

end;

thus great_eq_dom f,a is Subset of X by A13; :: thesis: verum