take V = {(0. X)}; :: thesis: ( not V is empty & V is symmetric )
thus not V is empty ; :: thesis: V is symmetric
thus V = - V by Th13; :: according to RLTOPSP1:def 5 :: thesis: verum