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