let C be non empty set ; :: thesis: for F being FuzzySet of C holds Core F = F " {1}
let F be FuzzySet of C; :: thesis: Core F = F " {1}
thus Core F c= F " {1} :: according to XBOOLE_0:def 10 :: thesis: F " {1} c= Core F

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Core F or x in F " {1} )
assume x in Core F ; :: thesis: x in F " {1}
then consider xx being Element of C such that
A1: ( x = xx & F . xx = 1 ) ;
A2: F . xx in {1} by TARSKI:def 1, A1;
dom F = C by FUNCT_2:def 1;
hence x in F " {1} by A1, FUNCT_1:def 7, A2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F " {1} or x in Core F )
assume a1: x in F " {1} ; :: thesis: x in Core F
then A1: ( x in dom F & F . x in {1} ) by FUNCT_1:def 7;
reconsider xx = x as Element of C by a1;
F . xx = 1 by A1, TARSKI:def 1;
hence x in Core F ; :: thesis: verum