let A, B be set ; for X being Subset of A
for R being Relation of A,B holds (R .: X) ` = (R `) .:^ X
let X be Subset of A; for R being Relation of A,B holds (R .: X) ` = (R `) .:^ X
let R be Relation of A,B; (R .: X) ` = (R `) .:^ X
thus
(R .: X) ` c= (R `) .:^ X
XBOOLE_0:def 10 (R `) .:^ X c= (R .: X) `
let a be object ; TARSKI:def 3 ( not a in (R `) .:^ X or a in (R .: X) ` )
assume A4:
a in (R `) .:^ X
; a in (R .: X) `
A5:
( a in (R `) .:^ X implies for x being set st x in X holds
not [x,a] in R )
proof
assume
a in (R `) .:^ X
;
for x being set st x in X holds
not [x,a] in R
let x be
set ;
( x in X implies not [x,a] in R )
assume A6:
x in X
;
not [x,a] in R
assume A7:
[x,a] in R
;
contradiction
a in Im (
(R `),
x)
by A4, A6, Th24;
then
ex
b being
object st
(
[b,a] in R ` &
b in {x} )
by RELAT_1:def 13;
then A8:
[x,a] in R `
by TARSKI:def 1;
R ` misses R
by XBOOLE_1:79;
hence
contradiction
by A7, A8, XBOOLE_0:3;
verum
end;
assume A9:
not a in (R .: X) `
; contradiction