let a be object ; :: according to FINSEQ_1:def 18 :: thesis: ( not a in {f} or a is set )
assume a in {f} ; :: thesis: a is set
hence a is set by TARSKI:def 1; :: thesis: verum