let X be set ; :: thesis: for x being object
for R being Relation holds
( x in dom (R | X) iff ( x in X & x in dom R ) )
let x be object ; :: thesis: for R being Relation holds
( x in dom (R | X) iff ( x in X & x in dom R ) )
let R be Relation; :: thesis: ( x in dom (R | X) iff ( x in X & x in dom R ) )
thus ( x in dom (R | X) implies ( x in X & x in dom R ) ) :: thesis: ( x in X & x in dom R implies x in dom (R | X) )
proof
assume x in dom (R | X) ; :: thesis: ( x in X & x in dom R )
then consider y being object such that
A1: [x,y] in R | X by XTUPLE_0:def 12;
[x,y] in R by A1, Def9;
hence ( x in X & x in dom R ) by A1, Def9, XTUPLE_0:def 12; :: thesis: verum
end;
assume A2: x in X ; :: thesis: ( not x in dom R or x in dom (R | X) )
assume x in dom R ; :: thesis: x in dom (R | X)
then consider y being object such that
A3: [x,y] in R by XTUPLE_0:def 12;
[x,y] in R | X by A2, A3, Def9;
hence x in dom (R | X) by XTUPLE_0:def 12; :: thesis: verum