let C be non empty set ; :: thesis: for F being FuzzySet of C
for alpha being Real holds alpha -cut F = F " [.alpha,1.]
let F be FuzzySet of C; :: thesis: for alpha being Real holds alpha -cut F = F " [.alpha,1.]
let alpha be Real; :: thesis: alpha -cut F = F " [.alpha,1.]
thus alpha -cut F c= F " [.alpha,1.] :: according to XBOOLE_0:def 10 :: thesis: F " [.alpha,1.] c= alpha -cut F

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in alpha -cut F or x in F " [.alpha,1.] )
assume x in alpha -cut F ; :: thesis: x in F " [.alpha,1.]
then consider y being Element of C such that
A1: ( x = y & F . y >= alpha ) ;
x in C by A1;
then A2: x in dom F by FUNCT_2:def 1;
then F . y in [.0,1.] by A1, PARTFUN1:4;
then ( 0 <= F . y & F . y <= 1 ) by XXREAL_1:1;
then F . y in [.alpha,1.] by A1;
hence x in F " [.alpha,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 " [.alpha,1.] or x in alpha -cut F )
assume c2: x in F " [.alpha,1.] ; :: thesis: x in alpha -cut F
then ( x in dom F & F . x in [.alpha,1.] ) by FUNCT_1:def 7;
then ( alpha <= F . x & F . x <= 1 ) by XXREAL_1:1;
hence x in alpha -cut F by c2; :: thesis: verum