let X, Y be set ; ( id (X \/ Y) = (id X) \/ (id Y) & id (X /\ Y) = (id X) /\ (id Y) & id (X \ Y) = (id X) \ (id Y) )
thus
id (X \/ Y) = (id X) \/ (id Y)
( id (X /\ Y) = (id X) /\ (id Y) & id (X \ Y) = (id X) \ (id Y) )proof
let x,
y be
object ;
RELAT_1:def 2 ( ( not [x,y] in id (X \/ Y) or [x,y] in (id X) \/ (id Y) ) & ( not [x,y] in (id X) \/ (id Y) or [x,y] in id (X \/ Y) ) )
thus
(
[x,y] in id (X \/ Y) implies
[x,y] in (id X) \/ (id Y) )
( not [x,y] in (id X) \/ (id Y) or [x,y] in id (X \/ Y) )
assume
[x,y] in (id X) \/ (id Y)
;
[x,y] in id (X \/ Y)
then A3:
(
[x,y] in id X or
[x,y] in id Y )
by XBOOLE_0:def 3;
then
(
x in X or
x in Y )
by RELAT_1:def 10;
then A4:
x in X \/ Y
by XBOOLE_0:def 3;
x = y
by A3, RELAT_1:def 10;
hence
[x,y] in id (X \/ Y)
by A4, RELAT_1:def 10;
verum
end;
thus
id (X /\ Y) = (id X) /\ (id Y)
id (X \ Y) = (id X) \ (id Y)proof
let x,
y be
object ;
RELAT_1:def 2 ( ( not [x,y] in id (X /\ Y) or [x,y] in (id X) /\ (id Y) ) & ( not [x,y] in (id X) /\ (id Y) or [x,y] in id (X /\ Y) ) )
thus
(
[x,y] in id (X /\ Y) implies
[x,y] in (id X) /\ (id Y) )
( not [x,y] in (id X) /\ (id Y) or [x,y] in id (X /\ Y) )proof
assume A5:
[x,y] in id (X /\ Y)
;
[x,y] in (id X) /\ (id Y)
then A6:
x in X /\ Y
by RELAT_1:def 10;
A7:
x = y
by A5, RELAT_1:def 10;
x in Y
by A6, XBOOLE_0:def 4;
then A8:
[x,y] in id Y
by A7, RELAT_1:def 10;
x in X
by A6, XBOOLE_0:def 4;
then
[x,y] in id X
by A7, RELAT_1:def 10;
hence
[x,y] in (id X) /\ (id Y)
by A8, XBOOLE_0:def 4;
verum
end;
assume A9:
[x,y] in (id X) /\ (id Y)
;
[x,y] in id (X /\ Y)
then A10:
[x,y] in id X
by XBOOLE_0:def 4;
then A11:
x = y
by RELAT_1:def 10;
[x,y] in id Y
by A9, XBOOLE_0:def 4;
then A12:
x in Y
by RELAT_1:def 10;
x in X
by A10, RELAT_1:def 10;
then
x in X /\ Y
by A12, XBOOLE_0:def 4;
hence
[x,y] in id (X /\ Y)
by A11, RELAT_1:def 10;
verum
end;
let x, y be object ; RELAT_1:def 2 ( ( not [x,y] in id (X \ Y) or [x,y] in (id X) \ (id Y) ) & ( not [x,y] in (id X) \ (id Y) or [x,y] in id (X \ Y) ) )
thus
( [x,y] in id (X \ Y) implies [x,y] in (id X) \ (id Y) )
( not [x,y] in (id X) \ (id Y) or [x,y] in id (X \ Y) )
assume A16:
[x,y] in (id X) \ (id Y)
; [x,y] in id (X \ Y)
then A17:
x = y
by RELAT_1:def 10;
not [x,y] in id Y
by A16, XBOOLE_0:def 5;
then A18:
( not x in Y or not x = y )
by RELAT_1:def 10;
x in X
by A16, RELAT_1:def 10;
then
x in X \ Y
by A16, A18, RELAT_1:def 10, XBOOLE_0:def 5;
hence
[x,y] in id (X \ Y)
by A17, RELAT_1:def 10; verum