let RS be strict RelStr ; :: thesis: UniformSpaceStr2RelStr (RelStr2UniformSpaceStr RS) = RS
set US = UniformSpaceStr2RelStr (RelStr2UniformSpaceStr RS);

now :: thesis: ( the carrier of (UniformSpaceStr2RelStr (RelStr2UniformSpaceStr RS)) = the carrier of RS & the InternalRel of (UniformSpaceStr2RelStr (RelStr2UniformSpaceStr RS)) = the InternalRel of RS )

thus the carrier of (UniformSpaceStr2RelStr (RelStr2UniformSpaceStr RS)) = the carrier of RS ; :: thesis: the InternalRel of (UniformSpaceStr2RelStr (RelStr2UniformSpaceStr RS)) = the InternalRel of RS
the InternalRel of (UniformSpaceStr2RelStr (RelStr2UniformSpaceStr RS)) = meet (rho the InternalRel of RS) ;
hence the InternalRel of (UniformSpaceStr2RelStr (RelStr2UniformSpaceStr RS)) = the InternalRel of RS by Th28; :: thesis: verum

end;

hence UniformSpaceStr2RelStr (RelStr2UniformSpaceStr RS) = RS ; :: thesis: verum