for x being set st x in dom c holds
x is real

proof

let x be set ; :: thesis: ( x in dom c implies x is real )
assume A1: x in dom c ; :: thesis: x is real
dom c c= REAL by Th24;
hence x is real by A1; :: thesis: verum

end;

hence dom c is real-membered by MEMBERED:def 3; :: thesis: verum