theorem :: RLVECT_1:1

for V being non empty 1-sorted
for v being Element of V holds v in V ;