let X be set ; :: thesis: X /\ (id ((proj1 X) /\ (proj2 X))) = X /\ (id (proj1 X))
set D = proj1 X;
set C = proj2 X;
set i = id ((proj1 X) /\ (proj2 X));
set I = id (proj1 X);
set R = X /\ (id (proj1 X));
set r = X /\ (id ((proj1 X) /\ (proj2 X)));
( X /\ (id ((proj1 X) /\ (proj2 X))) = X /\ ((id (proj1 X)) /\ (id (proj2 X))) & ((X /\ (id (proj1 X))) /\ (id (proj2 X))) \+\ (X /\ ((id (proj1 X)) /\ (id (proj2 X)))) = {} ) by SYSREL:14;
then reconsider r = X /\ (id ((proj1 X) /\ (proj2 X))) as Subset of (X /\ (id (proj1 X))) by Th29;
now :: thesis: for z being object st z in X /\ (id (proj1 X)) holds
z in r
let z be object ; :: thesis: ( z in X /\ (id (proj1 X)) implies z in r )
assume A1: z in X /\ (id (proj1 X)) ; :: thesis: z in r
consider x, y being object such that
A2: z = [x,y] by RELAT_1:def 1, A1;
A3: ( x in proj1 X & y in proj2 X ) by A1, A2, XTUPLE_0:def 12, XTUPLE_0:def 13;
A4: x = y by A2, A1, RELAT_1:def 10;
then x in (proj1 X) /\ (proj2 X) by A3, XBOOLE_0:def 4;
then [x,y] in id ((proj1 X) /\ (proj2 X)) by A4, RELAT_1:def 10;
hence z in r by A1, A2, XBOOLE_0:def 4; :: thesis: verum
end;
then X /\ (id (proj1 X)) c= r ;
hence X /\ (id ((proj1 X) /\ (proj2 X))) = X /\ (id (proj1 X)) ; :: thesis: verum