let L be non empty reflexive RelStr ; :: thesis: for c being closure Function of L,L
for x being Element of L holds c . x >= x
let c be closure Function of L,L; :: thesis: for x being Element of L holds c . x >= x
let x be Element of L; :: thesis: c . x >= x
c >= id L by WAYBEL_1:def 14;
then c . x >= (id L) . x by YELLOW_2:9;
hence c . x >= x ; :: thesis: verum