let e be object ; :: according to MEMBERED:def 3 :: thesis: ( not e in A "" or not e is V20() )
assume e in A "" ; :: thesis: e is V20()
then ex c being Complex st
( e = c " & c in A ) ;
hence e is V20() ; :: thesis: verum