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

hence not Convex-Family M is empty by A1, Def4; :: thesis: verum

proof

Up ((Omega). V) is convex
by Th9;
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;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

hence not Convex-Family M is empty by A1, Def4; :: thesis: verum