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:58;
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 ;
(incl (S,R)) . y = b by A1;
hence ( not x <= y or (incl (S,R)) . x <= (incl (S,R)) . y ) by A2, YELLOW_0:59; :: thesis: verum