let N be non empty reflexive RelStr ; :: thesis: id N is greater_or_equal_to_id
let j be Element of N; :: according to WAYBEL28:def 1 :: thesis: j <= (id N) . j
reconsider n = j as Element of N ;
n <= (id N) . n ;
hence j <= (id N) . j ; :: thesis: verum