let X be set ; for R being Relation st id X c= R \/ (R ~) holds
( id X c= R & id X c= R ~ )
let R be Relation; ( id X c= R \/ (R ~) implies ( id X c= R & id X c= R ~ ) )
assume A1:
id X c= R \/ (R ~)
; ( id X c= R & id X c= R ~ )
for x being object st x in X holds
( [x,x] in R & [x,x] in R ~ )
proof
let x be
object ;
( x in X implies ( [x,x] in R & [x,x] in R ~ ) )
assume
x in X
;
( [x,x] in R & [x,x] in R ~ )
then
[x,x] in id X
by RELAT_1:def 10;
then A2:
(
[x,x] in R or
[x,x] in R ~ )
by A1, XBOOLE_0:def 3;
hence
[x,x] in R
by RELAT_1:def 7;
[x,x] in R ~
thus
[x,x] in R ~
by A2, RELAT_1:def 7;
verum
end;
then
( ( for x being object st x in X holds
[x,x] in R ) & ( for x being object st x in X holds
[x,x] in R ~ ) )
;
hence
( id X c= R & id X c= R ~ )
by RELAT_1:47; verum