let R be Relation; id (field R) is_isomorphism_of R,R
A1:
now for a, b being object holds
( ( [a,b] in R implies ( a in field R & b in field R & [((id (field R)) . a),((id (field R)) . b)] in R ) ) & ( a in field R & b in field R & [((id (field R)) . a),((id (field R)) . b)] in R implies [a,b] in R ) )let a,
b be
object ;
( ( [a,b] in R implies ( a in field R & b in field R & [((id (field R)) . a),((id (field R)) . b)] in R ) ) & ( a in field R & b in field R & [((id (field R)) . a),((id (field R)) . b)] in R implies [a,b] in R ) )thus
(
[a,b] in R implies (
a in field R &
b in field R &
[((id (field R)) . a),((id (field R)) . b)] in R ) )
( a in field R & b in field R & [((id (field R)) . a),((id (field R)) . b)] in R implies [a,b] in R )assume that A4:
a in field R
and A5:
(
b in field R &
[((id (field R)) . a),((id (field R)) . b)] in R )
;
[a,b] in R
(id (field R)) . a = a
by A4, FUNCT_1:18;
hence
[a,b] in R
by A5, FUNCT_1:18;
verum end;
thus
id (field R) is_isomorphism_of R,R
by A1; verum