SupBelow (R,C) c= the carrier of L

proof

hence
SupBelow (R,C) is Subset of L
; :: thesis: verum
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;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