SupBelow (R,C) c= the carrier of L
proof
let x be object ; :: 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