let x be object ; for R1, R2 being Relation holds Im ((R1 \ R2),x) = (Im (R1,x)) \ (Im (R2,x))
let R1, R2 be Relation; Im ((R1 \ R2),x) = (Im (R1,x)) \ (Im (R2,x))
thus
Im ((R1 \ R2),x) c= (Im (R1,x)) \ (Im (R2,x))
XBOOLE_0:def 10 (Im (R1,x)) \ (Im (R2,x)) c= Im ((R1 \ R2),x)proof
let y be
object ;
TARSKI:def 3 ( not y in Im ((R1 \ R2),x) or y in (Im (R1,x)) \ (Im (R2,x)) )
assume
y in Im (
(R1 \ R2),
x)
;
y in (Im (R1,x)) \ (Im (R2,x))
then A1:
[x,y] in R1 \ R2
by Th9;
then A2:
not
[x,y] in R2
by XBOOLE_0:def 5;
A3:
y in Im (
R1,
x)
by A1, Th9;
not
y in Im (
R2,
x)
by A2, Th9;
hence
y in (Im (R1,x)) \ (Im (R2,x))
by A3, XBOOLE_0:def 5;
verum
end;
let y be object ; TARSKI:def 3 ( not y in (Im (R1,x)) \ (Im (R2,x)) or y in Im ((R1 \ R2),x) )
assume A4:
y in (Im (R1,x)) \ (Im (R2,x))
; y in Im ((R1 \ R2),x)
then A5:
not y in Im (R2,x)
by XBOOLE_0:def 5;
A6:
[x,y] in R1
by A4, Th9;
not [x,y] in R2
by A5, Th9;
then
[x,y] in R1 \ R2
by A6, XBOOLE_0:def 5;
hence
y in Im ((R1 \ R2),x)
by Th9; verum