theorem Th31: :: ISOMICHI:31

for a, b being Real holds IRRAT (a,b) c= [.a,+infty.[