let x, y be set ; :: thesis: for R being Relation holds
( ( R * R = R & R * (R \ (CL R)) = {} & [x,y] in R & x <> y implies ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) ) & ( R * R = R & (R \ (CL R)) * R = {} & [x,y] in R & x <> y implies ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) ) )
let R be Relation; :: thesis: ( ( R * R = R & R * (R \ (CL R)) = {} & [x,y] in R & x <> y implies ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) ) & ( R * R = R & (R \ (CL R)) * R = {} & [x,y] in R & x <> y implies ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) ) )
thus ( R * R = R & R * (R \ (CL R)) = {} & [x,y] in R & x <> y implies ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) ) :: thesis: ( R * R = R & (R \ (CL R)) * R = {} & [x,y] in R & x <> y implies ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) )

proof

assume A1: ( R * R = R & R * (R \ (CL R)) = {} & [x,y] in R & x <> y ) ; :: thesis: ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) )
then not [x,y] in id (dom R) by RELAT_1:def 10;
then not [x,y] in R /\ (id (dom R)) by XBOOLE_0:def 4;
then A2: [x,y] in R \ (CL R) by A1, XBOOLE_0:def 5;
consider z being set such that
A3: ( [x,z] in R & [z,y] in R ) by A1, RELAT_1:def 8;
z = y

proof

assume z <> y ; :: thesis: contradiction
then not [z,y] in id (dom R) by RELAT_1:def 10;
then not [z,y] in R /\ (id (dom R)) by XBOOLE_0:def 4;
then ( [x,z] in R & [z,y] in R \ (CL R) ) by A3, XBOOLE_0:def 5;
hence contradiction by A1, RELAT_1:def 8; :: thesis: verum

end;

then A4: ( y in rng R & y = z ) by A1, RELAT_1:20;
A5: not x in dom (CL R)

proof

assume x in dom (CL R) ; :: thesis: contradiction
then [x,x] in R by Th46;
hence contradiction by A1, A2, RELAT_1:def 8; :: thesis: verum

end;

x in dom R by A3, RELAT_1:20;
hence ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) by A3, A4, A5, Th46, XBOOLE_0:def 5; :: thesis: verum

end;

thus ( R * R = R & (R \ (CL R)) * R = {} & [x,y] in R & x <> y implies ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) ) :: thesis: verum

proof

assume A6: ( R * R = R & (R \ (CL R)) * R = {} & [x,y] in R & x <> y ) ; :: thesis: ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) )
then not [x,y] in id (dom R) by RELAT_1:def 10;
then not [x,y] in R /\ (id (dom R)) by XBOOLE_0:def 4;
then A7: [x,y] in R \ (CL R) by A6, XBOOLE_0:def 5;
consider z being set such that
A8: ( [x,z] in R & [z,y] in R ) by A6, RELAT_1:def 8;
z = x

proof

assume z <> x ; :: thesis: contradiction
then not [x,z] in id (dom R) by RELAT_1:def 10;
then not [x,z] in R /\ (id (dom R)) by XBOOLE_0:def 4;
then ( [z,y] in R & [x,z] in R \ (CL R) ) by A8, XBOOLE_0:def 5;
hence contradiction by A6, RELAT_1:def 8; :: thesis: verum

end;

then A9: ( x in dom R & x = z ) by A6, RELAT_1:20;
A10: not y in dom (CL R)

proof

assume y in dom (CL R) ; :: thesis: contradiction
then [y,y] in R by Th46;
hence contradiction by A6, A7, RELAT_1:def 8; :: thesis: verum

end;

y in rng R by A8, RELAT_1:20;
hence ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) by A8, A9, A10, Th46, XBOOLE_0:def 5; :: thesis: verum

end;