great_eq_dom (f,a) c= X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in great_eq_dom (f,a) or x in X )
assume x in great_eq_dom (f,a) ; :: thesis: x in X
then A4: x in dom f by Def14;
dom f c= X by RELAT_1:def 18;
hence x in X by A4; :: thesis: verum

end;

hence great_eq_dom (f,a) is Subset of X ; :: thesis: verum