let FT be non empty RelStr ; 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; 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; ( 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
;
( 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 A3, XBOOLE_0:def 4;
then A5:
y in U_FT x
by XBOOLE_0:def 5;
not
y in {x}
by A4, XBOOLE_0:def 5;
then
not
x = y
by TARSKI:def 1;
then A6:
P_e (
x,
y)
= FALSE
by Def5;
y in A
by A3, XBOOLE_0:def 4;
then A7:
P_1 (
x,
y,
A)
= TRUE
by A5, Def1;
x in A
by A2, FIN_TOPO:10;
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;
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 )
;
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 A11, Def5;
then A12:
not
y in {x}
by TARSKI:def 1;
y in U_FT x
by A10, Def1;
then A13:
y in (U_FT x) \ {x}
by A12, XBOOLE_0:def 5;
y in A
by A10, Def1;
then A14:
(U_FT x) \ {x} meets A
by A13, XBOOLE_0:3;
x in A
by A8, Def4;
hence
x in A ^n
by A14, FIN_TOPO:10;
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; verum