theorem Th1: :: LFUZZY_0:1

for X being real-membered set ex R being strict RelStr st
( the carrier of R = X & R is real )