reconsider F = {({} V)} as Subset-Family of V ;
take F ; :: thesis: ( not F is empty & F is circled-membered )
thus not F is empty ; :: thesis: F is circled-membered
let M be Subset of V; :: according to RLTOPSP1:def 7 :: thesis: ( M in F implies M is circled )
assume M in F ; :: thesis: M is circled
hence M is circled by TARSKI:def 1; :: thesis: verum