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 ( P_A (x,A) = TRUE & ex y being Element of FT st
( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) )

let x be Element of FT; :: thesis: for A being Subset of FT holds
( x in A ^n iff ( P_A (x,A) = TRUE & ex y being Element of FT st
( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) )

let A be Subset of FT; :: thesis: ( x in A ^n iff ( P_A (x,A) = TRUE & ex y being Element of FT st
( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) )

A1: ( x in A ^n implies ( P_A (x,A) = TRUE & ex y being Element of FT st
( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) )
proof
assume A2: x in A ^n ; :: thesis: ( P_A (x,A) = TRUE & ex y being Element of FT st
( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) )

then (U_FT x) \ {x} meets A by FIN_TOPO:10;
then ((U_FT x) \ {x}) /\ A <> {} ;
then consider y being Element of FT such that
A3: y in ((U_FT x) \ {x}) /\ A by SUBSET_1:4;
A4: y in (U_FT x) \ {x} by ;
then A5: y in U_FT x by XBOOLE_0:def 5;
not y in {x} by ;
then not x = y by TARSKI:def 1;
then A6: P_e (x,y) = FALSE by Def5;
y in A by ;
then A7: P_1 (x,y,A) = TRUE by ;
x in A by ;
hence ( P_A (x,A) = TRUE & ex y being Element of FT st
( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) by A6, A7, Def4; :: thesis: verum
end;
( P_A (x,A) = TRUE & ex y being Element of FT st
( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) implies x in A ^n )
proof
assume that
A8: P_A (x,A) = TRUE and
A9: ex y being Element of FT st
( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ; :: thesis: x in A ^n
consider y being Element of FT such that
A10: P_1 (x,y,A) = TRUE and
A11: P_e (x,y) = FALSE by A9;
x <> y by ;
then A12: not y in {x} by TARSKI:def 1;
y in U_FT x by ;
then A13: y in (U_FT x) \ {x} by ;
y in A by ;
then A14: (U_FT x) \ {x} meets A by ;
x in A by ;
hence x in A ^n by ; :: thesis: verum
end;
hence ( x in A ^n iff ( P_A (x,A) = TRUE & ex y being Element of FT st
( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) ) by A1; :: thesis: verum