let FT be non empty RelStr ; :: thesis: for x being Element of FT
for A being Subset of FT st x in A ^s holds
not x in (A \ {x}) ^b
let x be Element of FT; :: thesis: for A being Subset of FT st x in A ^s holds
not x in (A \ {x}) ^b
let A be Subset of FT; :: thesis: ( x in A ^s implies not x in (A \ {x}) ^b )
assume x in A ^s ; :: thesis: not x in (A \ {x}) ^b
then A misses (U_FT x) \ {x} by Th9;
then A /\ ((U_FT x) \ {x}) = {} ;
then A1: (A /\ (U_FT x)) \ {x} = {} by XBOOLE_1:49;

now :: thesis: A \ {x} misses U_FT x

per cases ( A /\ (U_FT x) = {} or A /\ (U_FT x) = {x} ) by A1, ZFMISC_1:58;

suppose A /\ (U_FT x) = {} ; :: thesis: A \ {x} misses U_FT x

then A misses U_FT x ;
hence A \ {x} misses U_FT x by XBOOLE_1:36, XBOOLE_1:63; :: thesis: verum

end;

suppose A /\ (U_FT x) = {x} ; :: thesis: A \ {x} misses U_FT x

then ((U_FT x) /\ A) \ {x} = {} by XBOOLE_1:37;
then (U_FT x) /\ (A \ {x}) = {} by XBOOLE_1:49;
hence A \ {x} misses U_FT x ; :: thesis: verum

end;

end;

end;

hence not x in (A \ {x}) ^b by Th8; :: thesis: verum