for
x
being
set
st
x
in
].
a
,
b
.[
holds
x
in
REAL
;
hence
].
a
,
b
.[
is
Subset
of
REAL
;
:: thesis:
verum