let A, B be set ; :: thesis: for X being Subset of A
for R being Relation of A,B holds
( X c= proj1 R iff X c= (R * (R ~)) .: X )
let X be Subset of A; :: thesis: for R being Relation of A,B holds
( X c= proj1 R iff X c= (R * (R ~)) .: X )
let R be Relation of A,B; :: thesis: ( X c= proj1 R iff X c= (R * (R ~)) .: X )
thus ( X c= proj1 R implies X c= (R * (R ~)) .: X ) :: thesis: ( X c= (R * (R ~)) .: X implies X c= proj1 R )

proof

assume A1: X c= proj1 R ; :: thesis: X c= (R * (R ~)) .: X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in (R * (R ~)) .: X )
assume A2: x in X ; :: thesis: x in (R * (R ~)) .: X
then reconsider x = x as Element of A ;
consider y being object such that
A3: [x,y] in R by A1, A2, XTUPLE_0:def 12;
A4: [y,x] in R ~ by A3, RELAT_1:def 7;
y in {y} by TARSKI:def 1;
then A5: x in (R ~) .: {y} by A4, RELAT_1:def 13;
(R ~) .: {y} c= (R * (R ~)) .: X

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (R ~) .: {y} or a in (R * (R ~)) .: X )
assume a in (R ~) .: {y} ; :: thesis: a in (R * (R ~)) .: X
then ex b being object st
( [b,a] in R ~ & b in {y} ) by RELAT_1:def 13;
then [y,a] in R ~ by TARSKI:def 1;
then [x,a] in R * (R ~) by A3, RELAT_1:def 8;
hence a in (R * (R ~)) .: X by A2, RELAT_1:def 13; :: thesis: verum

end;

hence x in (R * (R ~)) .: X by A5; :: thesis: verum

end;

assume A6: X c= (R * (R ~)) .: X ; :: thesis: X c= proj1 R
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in proj1 R )
assume x in X ; :: thesis: x in proj1 R
then A7: x in (R * (R ~)) .: X by A6;
A8: (R * (R ~)) .: X = (R ~) .: (R .: X) by RELAT_1:126;
(R ~) .: (R .: X) c= (R ~) .: B by RELAT_1:123;
then (R * (R ~)) .: X c= proj1 R by A8, Th50;
hence x in proj1 R by A7; :: thesis: verum