theorem Th52: :: CLASSES4:52

for N1, N2 being set st N1 = [:NAT,NAT:] \/ NAT & N2 = N1 \/ (bool N1) holds
REAL c= N2 \/ [:NAT,N2:]