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

proof

let x, y be set ; :: according to RELAT_1:def 2 :: thesis: ( [x,y] in dom {} iff [x,y] in {} )
thus ( [x,y] in dom {} implies [x,y] in {} ) :: thesis: ( [x,y] in {} implies [x,y] in dom {} )

proof

assume [x,y] in dom {} ; :: thesis: [x,y] in {}
then ex z being set st [[x,y],z] in {} ;
hence [x,y] in {} ; :: thesis: verum

end;

thus ( [x,y] in {} implies [x,y] in dom {} ) ; :: thesis: verum

end;

let x, y be set ; :: according to RELAT_1:def 2 :: thesis: ( [x,y] in rng {} iff [x,y] in {} )
thus ( [x,y] in rng {} implies [x,y] in {} ) :: thesis: ( [x,y] in {} implies [x,y] in rng {} )

proof

assume [x,y] in rng {} ; :: thesis: [x,y] in {}
then ex z being set st [z,[x,y]] in {} ;
hence [x,y] in {} ; :: thesis: verum

end;

thus ( [x,y] in {} implies [x,y] in rng {} ) ; :: thesis: verum