let X, Y be set ; :: thesis: ( 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) :: thesis: ( id (X /\ Y) = (id X) /\ (id Y) & id (X \ Y) = (id X) \ (id Y) )

proof

let x be set ; :: according to RELAT_1:def 2 :: thesis: for b₁ being set holds
( ( not [x,b₁] in id (X \/ Y) or [x,b₁] in (id X) \/ (id Y) ) & ( not [x,b₁] in (id X) \/ (id Y) or [x,b₁] in id (X \/ Y) ) )
let y be set ; :: thesis: ( ( 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) ) :: thesis: ( not [x,y] in (id X) \/ (id Y) or [x,y] in id (X \/ Y) )

proof

assume [x,y] in id (X \/ Y) ; :: thesis: [x,y] in (id X) \/ (id Y)
then ( x in X \/ Y & x = y ) by RELAT_1:def 10;
then ( ( x in X or x in Y ) & x = y ) by XBOOLE_0:def 3;
then ( [x,y] in id X or [x,y] in id Y ) by RELAT_1:def 10;
hence [x,y] in (id X) \/ (id Y) by XBOOLE_0:def 3; :: thesis: verum

end;

assume [x,y] in (id X) \/ (id Y) ; :: thesis: [x,y] in id (X \/ Y)
then ( [x,y] in id X or [x,y] in id Y ) by XBOOLE_0:def 3;
then ( ( x in X or x in Y ) & x = y ) by RELAT_1:def 10;
then ( x in X \/ Y & x = y ) by XBOOLE_0:def 3;
hence [x,y] in id (X \/ Y) by RELAT_1:def 10; :: thesis: verum

end;

thus id (X /\ Y) = (id X) /\ (id Y) :: thesis: id (X \ Y) = (id X) \ (id Y)

proof

let x be set ; :: according to RELAT_1:def 2 :: thesis: for b₁ being set holds
( ( not [x,b₁] in id (X /\ Y) or [x,b₁] in (id X) /\ (id Y) ) & ( not [x,b₁] in (id X) /\ (id Y) or [x,b₁] in id (X /\ Y) ) )
let y be set ; :: thesis: ( ( 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) ) :: thesis: ( not [x,y] in (id X) /\ (id Y) or [x,y] in id (X /\ Y) )

proof

assume [x,y] in id (X /\ Y) ; :: thesis: [x,y] in (id X) /\ (id Y)
then ( x in X /\ Y & x = y ) by RELAT_1:def 10;
then ( x in X & x in Y & x = y ) by XBOOLE_0:def 4;
then ( [x,y] in id X & [x,y] in id Y ) by RELAT_1:def 10;
hence [x,y] in (id X) /\ (id Y) by XBOOLE_0:def 4; :: thesis: verum

end;

assume [x,y] in (id X) /\ (id Y) ; :: thesis: [x,y] in id (X /\ Y)
then ( [x,y] in id X & [x,y] in id Y ) by XBOOLE_0:def 4;
then ( x in X & x in Y & x = y ) by RELAT_1:def 10;
then ( x in X /\ Y & x = y ) by XBOOLE_0:def 4;
hence [x,y] in id (X /\ Y) by RELAT_1:def 10; :: thesis: verum

end;

thus id (X \ Y) = (id X) \ (id Y) :: thesis: verum

proof

let x be set ; :: according to RELAT_1:def 2 :: thesis: for b₁ being set holds
( ( not [x,b₁] in id (X \ Y) or [x,b₁] in (id X) \ (id Y) ) & ( not [x,b₁] in (id X) \ (id Y) or [x,b₁] in id (X \ Y) ) )
let y be set ; :: thesis: ( ( 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) ) :: thesis: ( not [x,y] in (id X) \ (id Y) or [x,y] in id (X \ Y) )

proof

assume [x,y] in id (X \ Y) ; :: thesis: [x,y] in (id X) \ (id Y)
then ( x in X \ Y & x = y ) by RELAT_1:def 10;
then ( x in X & not x in Y & x = y ) by XBOOLE_0:def 5;
then ( [x,y] in id X & not [x,y] in id Y ) by RELAT_1:def 10;
hence [x,y] in (id X) \ (id Y) by XBOOLE_0:def 5; :: thesis: verum

end;

assume [x,y] in (id X) \ (id Y) ; :: thesis: [x,y] in id (X \ Y)
then ( [x,y] in id X & not [x,y] in id Y ) by XBOOLE_0:def 5;
then ( x in X & x = y & ( not x in Y or not x = y ) ) by RELAT_1:def 10;
then ( x in X \ Y & x = y ) by XBOOLE_0:def 5;
hence [x,y] in id (X \ Y) by RELAT_1:def 10; :: thesis: verum

end;