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