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 )

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

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 that
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;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

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