let FT be non empty RelStr ; :: thesis: for x being Element of FT
for A being Subset of FT holds
( x in A ^n iff ( x in A & (U_FT x) \ {x} meets A ) )
let x be Element of FT; :: thesis: for A being Subset of FT holds
( x in A ^n iff ( x in A & (U_FT x) \ {x} meets A ) )
let A be Subset of FT; :: thesis: ( x in A ^n iff ( x in A & (U_FT x) \ {x} meets A ) )
thus ( x in A ^n implies ( x in A & (U_FT x) \ {x} meets A ) ) :: thesis: ( x in A & (U_FT x) \ {x} meets A implies x in A ^n )

proof

assume x in A ^n ; :: thesis: ( x in A & (U_FT x) \ {x} meets A )
then ( x in A & not x in A ^s ) by XBOOLE_0:def 5;
hence ( x in A & (U_FT x) \ {x} meets A ) ; :: thesis: verum

end;

assume that
A1: x in A and
A2: (U_FT x) \ {x} meets A ; :: thesis: x in A ^n
not x in A ^s by A2, Th9;
hence x in A ^n by A1, XBOOLE_0:def 5; :: thesis: verum