A1: M c= Up ((Omega). V)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in M or x in Up ((Omega). V) )
assume x in M ; :: thesis: x in Up ((Omega). V)
then reconsider x = x as Element of V ;
x in the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ;
then x in the carrier of ((Omega). V) by RLSUB_1:def 4;
hence x in Up ((Omega). V) by RUSUB_4:def 5; :: thesis: verum

end;

Up ((Omega). V) is convex by Th9;
hence not Convex-Family M is empty by A1, Def4; :: thesis: verum