SupBelow R,C c= the carrier of L

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in SupBelow R,C or x in the carrier of L )
assume x in SupBelow R,C ; :: thesis: x in the carrier of L
then x = sup (SetBelow R,C,x) by Def10;
hence x in the carrier of L ; :: thesis: verum

end;

hence SupBelow R,C is Subset of L ; :: thesis: verum