theorem Th5: :: TOPALG_7:5

[:R^1,R^1:] | [:(R^1 [.0,1.]),(R^1 [.0,1.]):] = [:I[01],I[01]:]