let A be non empty set ; for R being Relation of [:A,A:] st R is_reflexive_in [:A,A:] holds
id A is_FormalIz_of R
let R be Relation of [:A,A:]; ( R is_reflexive_in [:A,A:] implies id A is_FormalIz_of R )
assume A1:
for x being object st x in [:A,A:] holds
[x,x] in R
; RELAT_2:def 1 id A is_FormalIz_of R
let x be Element of A; TRANSGEO:def 2 for y being Element of A holds [[x,y],[((id A) . x),((id A) . y)]] in R
let y be Element of A; [[x,y],[((id A) . x),((id A) . y)]] in R
A2:
[x,y] in [:A,A:]
by ZFMISC_1:def 2;
thus
[[x,y],[((id A) . x),((id A) . y)]] in R
by A1, A2; verum