thus dom {} = {} :: thesis: rng {} = {}

proof

thus dom {} c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= dom {}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom {} or x in {} )
assume x in dom {} ; :: thesis: x in {}
then ex y being set st [x,y] in {} by Def4;
hence x in {} ; :: thesis: verum

end;

thus {} c= dom {} by XBOOLE_1:2; :: thesis: verum

end;

thus rng {} c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= rng {}

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng {} or y in {} )
assume y in rng {} ; :: thesis: y in {}
then ex x being set st [x,y] in {} by Def5;
hence y in {} ; :: thesis: verum

end;

thus {} c= rng {} by XBOOLE_1:2; :: thesis: verum