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

assume A1: x in dom c ; :: thesis: x is real

dom c c= REAL by Th24;

hence x is real by A1; :: thesis: verum