environ
vocabularies ENUMSET,RELATION;
notations ENUMSET,RELATION;
constructors ENUMSET,RELATION;
definitions ENUMSET,RELATION;
equalities ENUMSET,RELATION;
theorems ENUMSET,RELATION;
begin
reserve a,b,x,y,z,A,B,C for set, P,Q,R,S,T for Relation;
:: 4.31
R c= R~ iff R = R~
proof
thus R c= R~ implies R = R~
proof
assume r: R c= R~;
hence R c= R~;
thus R~ c= R
proof
let x,y be set;
assume [x,y] in R~;
then [y,x] in R by RELATION:def 3;
then [y,x] in R~ by r,RELATION:def 9;
hence [x,y] in R by RELATION:def 3;
end;
end;
thus R = R~ implies R c= R~ by RELATION:def 10;
end;
:: 4.32a
(R\/S)~ = (R~)\/(S~)
proof
thus (R\/S)~ c= (R~)\/(S~)
proof
let x,y be set;
assume [x,y] in (R\/S)~;
then [y,x] in R\/S by RELATION:def 3;
then [y,x] in R or [y,x] in S by RELATION:def 4;
then [x,y] in R~ or [x,y] in S~ by RELATION:def 3;
hence [x,y] in (R~)\/(S~) by RELATION:def 4;
end;
thus (R~)\/(S~) c= (R\/S)~
proof
let x,y be set;
assume [x,y] in (R~)\/(S~);
then [x,y] in R~ or [x,y] in S~ by RELATION:def 4;
then [y,x] in R or [y,x] in S by RELATION:def 3;
then [y,x] in R\/S by RELATION:def 4;
hence [x,y] in (R\/S)~ by RELATION:def 3;
end;
end;
:: 4.32b
(R/\S)~ = (R~)/\(S~)
proof
thus (R/\S)~ c= (R~)/\(S~)
proof
let x,y be set;
assume [x,y] in (R/\S)~;
then [y,x] in R/\S by RELATION:def 3;
then [y,x] in R & [y,x] in S by RELATION:def 5;
then [x,y] in R~ & [x,y] in S~ by RELATION:def 3;
hence [x,y] in (R~)/\(S~) by RELATION:def 5;
end;
thus (R~)/\(S~) c= (R/\S)~
proof
let x,y be set;
assume [x,y] in (R~)/\(S~);
then [x,y] in R~ & [x,y] in S~ by RELATION:def 5;
then [y,x] in R & [y,x] in S by RELATION:def 3;
then [y,x] in R/\S by RELATION:def 5;
hence [x,y] in (R/\S)~ by RELATION:def 3;
end;
end;
:: 4.41
R*(S*T) = (R*S)*T
proof
thus R*(S*T) c= (R*S)*T
proof
let x,y;
assume [x,y] in R*(S*T);
then consider a such that
a: [x,a] in R & [a,y] in S*T by RELATION:def 7;
consider b such that
b: [a,b] in S & [b,y] in T by a,RELATION:def 7;
[x,b] in R*S by a,b,RELATION:def 7;
hence [x,y] in (R*S)*T by b,RELATION:def 7;
end;
thus (R*S)*T c= R*(S*T)
proof
let x,y;
assume [x,y] in (R*S)*T;
then consider a such that
a: [x,a] in R*S & [a,y] in T by RELATION:def 7;
consider b such that
b: [x,b] in R & [b,a] in S by a,RELATION:def 7;
[b,y] in S*T by a,b,RELATION:def 7;
hence [x,y] in R*(S*T) by b,RELATION:def 7;
end;
end;
:: 4.42
(R*S)~ = (S~)*(R~)
proof
thus (R*S)~ c= (S~)*(R~)
proof
let x,y;
assume [x,y] in (R*S)~;
then [y,x] in R*S by RELATION:def 3;
then consider a such that
a: [y,a] in R & [a,x] in S by RELATION:def 7;
[a,y] in R~ & [x,a] in S~ by a,RELATION:def 3;
hence [x,y] in (S~)*(R~) by RELATION:def 7;
end;
thus (S~)*(R~) c= (R*S)~
proof
let x,y;
assume [x,y] in (S~)*(R~);
then consider a such that
a: [x,a] in S~ & [a,y] in R~ by RELATION:def 7;
[a,x] in S & [y,a] in R by a,RELATION:def 3;
then [y,x] in R*S by RELATION:def 7;
hence [x,y] in (R*S)~ by RELATION:def 3;
end;
end;
lr: {} c= R
proof
let x,y;
assume [x,y] in {};
hence thesis by RELATION:def 2;
end;
{}~ = {}
proof
thus {}~ c= {}
proof
let x,y;
assume [x,y] in {}~;
then [y,x] in {} by RELATION:def 3;
hence thesis by RELATION:def 2;
end;
thus {} c= {}~ by lr;
end;
R*{} = {}
proof
thus R*{} c= {}
proof
let x,y;
assume [x,y] in R*{};
then consider a such that
a: [x,a] in R & [a,y] in {} by RELATION:def 7;
thus thesis by a,RELATION:def 2;
end;
thus {} c= R*{} by lr;
end;
{}*R = {}
proof
thus {}*R c= {}
proof
let x,y;
assume [x,y] in {}*R;
then consider a such that
a: [x,a] in {} & [a,y] in R by RELATION:def 7;
thus thesis by a,RELATION:def 2;
end;
thus {} c= {}*R by lr;
end;