let x, y be Element of S; :: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or (corestr f) . x <= (corestr f) . y )
A1: f . y = (corestr f) . y by WAYBEL_1:30;
assume x <= y ; :: thesis: (corestr f) . x <= (corestr f) . y
then A2: f . x <= f . y by WAYBEL_1:def 2;
f . x = (corestr f) . x by WAYBEL_1:30;
hence (corestr f) . x <= (corestr f) . y by A2, A1, YELLOW_0:60; :: thesis: verum