theorem Th54: :: RUSUB_2:54

for V being RealUnitarySpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is Lattice