let L1, L2 be non empty RelStr ; :: thesis: for f being Function of L1,L2 st L2 is reflexive holds
f <= f
let f be Function of L1,L2; :: thesis: ( L2 is reflexive implies f <= f )
assume L2 is reflexive ; :: thesis: f <= f
then for x being Element of L1 holds f . x <= f . x ;
hence f <= f by YELLOW_2:9; :: thesis: verum