let x, y be Element of L; :: according to WAYBEL_4:def 4 :: thesis: ( [x,y] in IntRel L implies x <= y )
assume [x,y] in IntRel L ; :: thesis: x <= y
hence x <= y by ORDERS_2:def 9; :: thesis: verum