(R " {y}) /\ C c= the carrier of L ;
hence SetBelow (R,C,y) is Subset of L ; :: thesis: verum