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;

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

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