let FT be non empty RelStr ; :: thesis: for x being Element of FT
for A being Subset of FT holds
( x in A ^s iff ( P_A x,A = TRUE & ( for y being Element of FT holds
( not P_1 x,y,A = TRUE or not P_e x,y = FALSE ) ) ) )
let x be Element of FT; :: thesis: for A being Subset of FT holds
( x in A ^s iff ( P_A x,A = TRUE & ( for y being Element of FT holds
( not P_1 x,y,A = TRUE or not P_e x,y = FALSE ) ) ) )
let A be Subset of FT; :: thesis: ( x in A ^s iff ( P_A x,A = TRUE & ( for y being Element of FT holds
( not P_1 x,y,A = TRUE or not P_e x,y = FALSE ) ) ) )
A1: ( x in A ^s implies ( P_A x,A = TRUE & ( for y being Element of FT holds
( not P_1 x,y,A = TRUE or not P_e x,y = FALSE ) ) ) )

proof

assume x in A ^s ; :: thesis: ( P_A x,A = TRUE & ( for y being Element of FT holds
( not P_1 x,y,A = TRUE or not P_e x,y = FALSE ) ) )
then A2: ( x in A & (U_FT x) \ {x} misses A ) by FIN_TOPO:14;
then A3: ( x in A & ((U_FT x) \ {x}) /\ A = {} ) by XBOOLE_0:def 7;
for y being Element of FT holds
( not P_1 x,y,A = TRUE or not P_e x,y = FALSE )

proof

given y being Element of FT such that A4: P_1 x,y,A = TRUE and
A5: P_e x,y = FALSE ; :: thesis: contradiction
A6: ( y in U_FT x & y in A ) by A4, Def1;
not x = y by A5, Def5;
then not y in {x} by TARSKI:def 1;
then y in (U_FT x) \ {x} by A6, XBOOLE_0:def 5;
hence contradiction by A3, A6, XBOOLE_0:def 4; :: thesis: verum

end;

hence ( P_A x,A = TRUE & ( for y being Element of FT holds
( not P_1 x,y,A = TRUE or not P_e x,y = FALSE ) ) ) by A2, Def4; :: thesis: verum

end;

( P_A x,A = TRUE & ( for y being Element of FT holds
( not P_1 x,y,A = TRUE or not P_e x,y = FALSE ) ) implies x in A ^s )

proof

assume A7: ( P_A x,A = TRUE & ( for y being Element of FT holds
( not P_1 x,y,A = TRUE or not P_e x,y = FALSE ) ) ) ; :: thesis: x in A ^s
then A8: x in A by Def4;
for y being Element of FT holds not y in ((U_FT x) \ {x}) /\ A

proof

let y be Element of FT; :: thesis: not y in ((U_FT x) \ {x}) /\ A
( not P_1 x,y,A = TRUE or not P_e x,y = FALSE ) by A7;
then ( not y in U_FT x or x = y or not y in A ) by Def1, Def5;
then ( not y in U_FT x or y in {x} or not y in A ) by TARSKI:def 1;
then ( not y in (U_FT x) \ {x} or not y in A ) by XBOOLE_0:def 5;
hence not y in ((U_FT x) \ {x}) /\ A by XBOOLE_0:def 4; :: thesis: verum

end;

then ((U_FT x) \ {x}) /\ A = {} by SUBSET_1:10;
then (U_FT x) \ {x} misses A by XBOOLE_0:def 7;
hence x in A ^s by A8; :: thesis: verum

end;

hence ( x in A ^s iff ( P_A x,A = TRUE & ( for y being Element of FT holds
( not P_1 x,y,A = TRUE or not P_e x,y = FALSE ) ) ) ) by A1; :: thesis: verum