let A be non empty set ; :: thesis: 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:]; :: thesis: ( 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 ; :: according to RELAT_2:def 1 :: thesis: id A is_FormalIz_of R
let x be Element of A; :: according to TRANSGEO:def 2 :: thesis: for y being Element of A holds [[x,y],[((id A) . x),((id A) . y)]] in R
let y be Element of A; :: thesis: [[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; :: thesis: verum