theorem :: RLSUB_1:76

for V being RealLinearSpace
for V1 being Subset of V st V1 is Coset of (Omega). V holds
V1 = the carrier of V