let x, y be object ; :: 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 that
A1: R * R = R and
A2: R * (R \ (CL R)) = {} and
A3: [x,y] in R and
A4: x <> y ; :: thesis: ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) )
A5: y in rng R by A3, XTUPLE_0:def 13;
consider z being object such that
A6: [x,z] in R and
A7: [z,y] in R by A1, A3, RELAT_1:def 8;
A8: 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 [z,y] in R \ (CL R) by A7, XBOOLE_0:def 5;
hence contradiction by A2, A6, RELAT_1:def 8; :: thesis: verum
end;
not [x,y] in id (dom R) by A4, RELAT_1:def 10;
then not [x,y] in R /\ (id (dom R)) by XBOOLE_0:def 4;
then A9: [x,y] in R \ (CL R) by A3, XBOOLE_0:def 5;
A10: not x in dom (CL R)
proof
assume x in dom (CL R) ; :: thesis: contradiction
then [x,x] in R by Th27;
hence contradiction by A2, A9, RELAT_1:def 8; :: thesis: verum
end;
x in dom R by A6, XTUPLE_0:def 12;
hence ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) by A7, A8, A5, A10, Th27, 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 that
A11: R * R = R and
A12: (R \ (CL R)) * R = {} and
A13: [x,y] in R and
A14: x <> y ; :: thesis: ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) )
A15: x in dom R by A13, XTUPLE_0:def 12;
consider z being object such that
A16: [x,z] in R and
A17: [z,y] in R by A11, A13, RELAT_1:def 8;
A18: 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 [x,z] in R \ (CL R) by A16, XBOOLE_0:def 5;
hence contradiction by A12, A17, RELAT_1:def 8; :: thesis: verum
end;
not [x,y] in id (dom R) by A14, RELAT_1:def 10;
then not [x,y] in R /\ (id (dom R)) by XBOOLE_0:def 4;
then A19: [x,y] in R \ (CL R) by A13, XBOOLE_0:def 5;
A20: not y in dom (CL R)
proof
assume y in dom (CL R) ; :: thesis: contradiction
then [y,y] in R by Th27;
hence contradiction by A12, A19, RELAT_1:def 8; :: thesis: verum
end;
y in rng R by A17, XTUPLE_0:def 13;
hence ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) by A16, A18, A15, A20, Th27, XBOOLE_0:def 5; :: thesis: verum
end;