let C be non empty set ; :: thesis: for F being FuzzySet of C holds Core F = 1 -cut F
let F be FuzzySet of C; :: thesis: Core F = 1 -cut F
1 -cut F = F " [.1,1.] by AlphaCut1
.= F " {1} by XXREAL_1:17 ;
hence Core F = 1 -cut F by CCounter; :: thesis: verum