let x be object ; :: according to MEMBERED:def 3 :: thesis: ( not x in dom c or 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