for N being Subset of V st N in Circled-Family M holds
N is circled by Def2;
then Circled-Family M is circled-membered by RLTOPSP1:def 7;
hence meet (Circled-Family M) is circled Subset of V by RLTOPSP1:30; :: thesis: verum