Assume x  > y               # Antecedent assumption

    Then x ≥ ⌊x⌋            # By definition

    Then x ≥ z              # By definition

    Then ⌊x⌋≥ z             # Also by definition

    Let z = ⌊y⌋             # By assumption & definition since ∀z ∈ ℤ, y ∈ ℝ and ℤ ∈ ℝ

    Then ⌊x⌋ ≥ ⌊y⌋          # Substitution

Then x  > y  ⇒ ⌊x⌋ ≥ ⌊y⌋    # Introduce implication