let x, y be Element of S; :: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or (incl S,R) . x <= (incl S,R) . y )
reconsider a = x, b = y as Element of R by YELLOW_0:59;
the carrier of S c= the carrier of R by YELLOW_0:def 13;
then A1: incl S,R = id the carrier of S by Def1;
then A2: (incl S,R) . x = a by FUNCT_1:35;
(incl S,R) . y = b by A1, FUNCT_1:35;
hence ( not x <= y or (incl S,R) . x <= (incl S,R) . y ) by A2, YELLOW_0:60; :: thesis: verum