let A, B be set ; :: thesis: for Y being Subset of B
for R being Relation of A,B holds
( Y c= proj2 R iff Y c= ((R ~) * R) .: Y )
let Y be Subset of B; :: thesis: for R being Relation of A,B holds
( Y c= proj2 R iff Y c= ((R ~) * R) .: Y )
let R be Relation of A,B; :: thesis: ( Y c= proj2 R iff Y c= ((R ~) * R) .: Y )
thus ( Y c= proj2 R implies Y c= ((R ~) * R) .: Y ) :: thesis: ( Y c= ((R ~) * R) .: Y implies Y c= proj2 R )
proof
assume A1: Y c= proj2 R ; :: thesis: Y c= ((R ~) * R) .: Y
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in ((R ~) * R) .: Y )
assume A2: y in Y ; :: thesis: y in ((R ~) * R) .: Y
then consider x being object such that
A3: [x,y] in R by A1, XTUPLE_0:def 13;
A4: [y,x] in R ~ by A3, RELAT_1:def 7;
A5: y in Im (R,x) by A3, Th9;
R .: {x} c= ((R ~) * R) .: Y
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in R .: {x} or a in ((R ~) * R) .: Y )
assume a in R .: {x} ; :: thesis: a in ((R ~) * R) .: Y
then ex b being object st
( [b,a] in R & b in {x} ) by RELAT_1:def 13;
then [x,a] in R by TARSKI:def 1;
then [y,a] in (R ~) * R by A4, RELAT_1:def 8;
hence a in ((R ~) * R) .: Y by A2, RELAT_1:def 13; :: thesis: verum
end;
hence y in ((R ~) * R) .: Y by A5; :: thesis: verum
end;
assume A6: Y c= ((R ~) * R) .: Y ; :: thesis: Y c= proj2 R
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in proj2 R )
assume x in Y ; :: thesis: x in proj2 R
then A7: x in ((R ~) * R) .: Y by A6;
A8: ((R ~) * R) .: Y = R .: ((R ~) .: Y) by RELAT_1:126;
R .: ((R ~) .: Y) c= R .: A by RELAT_1:123;
then ((R ~) * R) .: Y c= proj2 R by A8, Th50;
hence x in proj2 R by A7; :: thesis: verum