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 ) ) ) )

( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) implies x in A ^s )

( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) ) ) by A1; :: thesis: verum

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

( P_A (x,A) = TRUE & ( for y being Element of FT holds
assume A2:
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 (U_FT x) \ {x} misses A by FIN_TOPO:9;

then A3: ((U_FT x) \ {x}) /\ A = {} ;

A4: for y being Element of FT holds

( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE )

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 A4, Def4; :: thesis: verum

end;( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) )

then (U_FT x) \ {x} misses A by FIN_TOPO:9;

then A3: ((U_FT x) \ {x}) /\ A = {} ;

A4: for y being Element of FT holds

( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE )

proof

x in A
by A2, FIN_TOPO:9;
given y being Element of FT such that A5:
P_1 (x,y,A) = TRUE
and

A6: P_e (x,y) = FALSE ; :: thesis: contradiction

not x = y by A6, Def5;

then A7: not y in {x} by TARSKI:def 1;

y in U_FT x by A5, Def1;

then A8: y in (U_FT x) \ {x} by A7, XBOOLE_0:def 5;

y in A by A5, Def1;

hence contradiction by A3, A8, XBOOLE_0:def 4; :: thesis: verum

end;A6: P_e (x,y) = FALSE ; :: thesis: contradiction

not x = y by A6, Def5;

then A7: not y in {x} by TARSKI:def 1;

y in U_FT x by A5, Def1;

then A8: y in (U_FT x) \ {x} by A7, XBOOLE_0:def 5;

y in A by A5, Def1;

hence contradiction by A3, A8, XBOOLE_0:def 4; :: thesis: verum

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 A4, Def4; :: thesis: verum

( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) implies x in A ^s )

proof

hence
( x in A ^s iff ( P_A (x,A) = TRUE & ( for y being Element of FT holds
assume that

A9: P_A (x,A) = TRUE and

A10: 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

for y being Element of FT holds not y in ((U_FT x) \ {x}) /\ A

then A11: (U_FT x) \ {x} misses A ;

x in A by A9, Def4;

hence x in A ^s by A11; :: thesis: verum

end;A9: P_A (x,A) = TRUE and

A10: 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

for y being Element of FT holds not y in ((U_FT x) \ {x}) /\ A

proof

then
((U_FT x) \ {x}) /\ A = {}
by SUBSET_1:4;
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 A10;

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;( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) by A10;

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

then A11: (U_FT x) \ {x} misses A ;

x in A by A9, Def4;

hence x in A ^s by A11; :: thesis: verum

( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) ) ) by A1; :: thesis: verum