let V be RealUnitarySpace; :: thesis: LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is 01_Lattice
LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is lower-bounded upper-bounded Lattice by Th55, Th56;
hence LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is 01_Lattice ; :: thesis: verum