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 set ; :: 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 set such that
A3: [x,y] in R by A1, A2, RELAT_1:def 4;
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 set ; :: 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 set 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 set ; :: 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:159;
(R ~ ) .: (R .: X) c= (R ~ ) .: B by RELAT_1:156;
then (R * (R ~ )) .: X c= proj1 R by A8, Th51;
hence x in proj1 R by A7; :: thesis: verum