[:
{
0
}
,
RAT+
:]
c=
[:
{
0
}
,
REAL+
:]
by
ARYTM_2:1
,
ZFMISC_1:95
;
then
RAT+
\/
[:
{
0
}
,
RAT+
:]
c=
REAL+
\/
[:
{
0
}
,
REAL+
:]
by
ARYTM_2:1
,
XBOOLE_1:13
;
hence
RAT
c=
REAL
by
XBOOLE_1:33
;
:: thesis:
verum