let C be non empty set ; :: thesis: Core (UMF C) = C
thus Core (UMF C) c= C ; :: according to XBOOLE_0:def 10 :: thesis: C c= Core (UMF C)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in C or x in Core (UMF C) )
assume x in C ; :: thesis: x in Core (UMF C)
then reconsider xx = x as Element of C ;
(UMF C) . xx = 1 by FUNCT_3:def 3;
hence x in Core (UMF C) ; :: thesis: verum