dom (Swap (f,a,b)) = dom f by FUNCT_7:99;
hence dom (Swap (f,a,b)) c= X ; :: according to RELAT_1:def 18 :: thesis: verum