let X be set ; :: thesis: for R being Relation st id X c= R \/ (R ~) holds
( id X c= R & id X c= R ~ )
let R be Relation; :: thesis: ( id X c= R \/ (R ~) implies ( id X c= R & id X c= R ~ ) )
assume A1: id X c= R \/ (R ~) ; :: thesis: ( 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 ; :: thesis: ( x in X implies ( [x,x] in R & [x,x] in R ~ ) )
assume x in X ; :: thesis: ( [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; :: thesis: [x,x] in R ~
thus [x,x] in R ~ by A2, RELAT_1:def 7; :: thesis: 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; :: thesis: verum