let X be set ; :: thesis: for O being Order of X holds
( dom O = X & rng O = X )
let O be Order of X; :: thesis: ( dom O = X & rng O = X )
thus dom O = X :: thesis: rng O = X

proof

thus dom O c= X ; :: according to XBOOLE_0:def 10 :: thesis: X c= dom O
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in dom O )
assume x in X ; :: thesis: x in dom O
then [x,x] in O by Th3;
hence x in dom O by XTUPLE_0:def 12; :: thesis: verum

end;

thus rng O c= X ; :: according to XBOOLE_0:def 10 :: thesis: X c= rng O
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in rng O )
assume x in X ; :: thesis: x in rng O
then [x,x] in O by Th3;
hence x in rng O by XTUPLE_0:def 13; :: thesis: verum