let C be non empty set ; :: thesis: Core (EMF C) = {}
thus Core (EMF C) c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= Core (EMF C)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Core (EMF C) or x in {} )
assume x in Core (EMF C) ; :: thesis: x in {}
then consider xx being Element of C such that
A1: ( x = xx & (EMF C) . xx = 1 ) ;
thus x in {} by A1, FUNCT_3:def 3; :: thesis: verum
end;
thus {} c= Core (EMF C) ; :: thesis: verum