theorem Th6: :: VECTSP_8:6

for F being Field
for VS being strict VectSp of F
for p, q being Element of (lattice VS)
for H1, H2 being strict Subspace of VS st p = H1 & q = H2 holds
( p [= q iff the carrier of H1 c= the carrier of H2 )