theorem Th57: :: RLSUB_2:57

for V being RealLinearSpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is 01_Lattice