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

proof

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

end;

Up ((Omega). V) is circled by Th6;
hence not Circled-Family M is empty by A1, Def2; :: thesis: verum