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

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