let X be set ; :: thesis: for C being non empty set

for c being Element of C holds

( c in C \ X iff (chi (X,C)) . c = 0 )

let C be non empty set ; :: thesis: for c being Element of C holds

( c in C \ X iff (chi (X,C)) . c = 0 )

let c be Element of C; :: thesis: ( c in C \ X iff (chi (X,C)) . c = 0 )

thus ( c in C \ X implies (chi (X,C)) . c = 0 ) :: thesis: ( (chi (X,C)) . c = 0 implies c in C \ X )

then not c in X by Th61;

hence c in C \ X by XBOOLE_0:def 5; :: thesis: verum

for c being Element of C holds

( c in C \ X iff (chi (X,C)) . c = 0 )

let C be non empty set ; :: thesis: for c being Element of C holds

( c in C \ X iff (chi (X,C)) . c = 0 )

let c be Element of C; :: thesis: ( c in C \ X iff (chi (X,C)) . c = 0 )

thus ( c in C \ X implies (chi (X,C)) . c = 0 ) :: thesis: ( (chi (X,C)) . c = 0 implies c in C \ X )

proof

assume
(chi (X,C)) . c = 0
; :: thesis: c in C \ X
assume
c in C \ X
; :: thesis: (chi (X,C)) . c = 0

then not c in X by XBOOLE_0:def 5;

hence (chi (X,C)) . c = 0 by Th61; :: thesis: verum

end;then not c in X by XBOOLE_0:def 5;

hence (chi (X,C)) . c = 0 by Th61; :: thesis: verum

then not c in X by Th61;

hence c in C \ X by XBOOLE_0:def 5; :: thesis: verum