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
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 A2:
(
x in A &
(U_FT x) \ {x} meets A )
by FIN_TOPO:15;
then
(
x in A &
((U_FT x) \ {x}) /\ A <> {} )
by XBOOLE_0:def 7;
then consider y being
Element of
FT such that A3:
y in ((U_FT x) \ {x}) /\ A
by SUBSET_1:10;
A4:
(
y in (U_FT x) \ {x} &
y in A )
by A3, XBOOLE_0:def 4;
then A5:
(
y in U_FT x & not
y in {x} )
by XBOOLE_0:def 5;
then
not
x = y
by TARSKI:def 1;
then A6:
P_e x,
y = FALSE
by Def5;
P_1 x,
y,
A = TRUE
by A4, A5, Def1;
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 A2, A6, 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 A7:
(
P_A x,
A = TRUE & ex
y being
Element of
FT st
(
P_1 x,
y,
A = TRUE &
P_e x,
y = FALSE ) )
;
:: thesis: x in A ^n
then A8:
x in A
by Def4;
consider y being
Element of
FT such that A9:
(
P_1 x,
y,
A = TRUE &
P_e x,
y = FALSE )
by A7;
(
y in U_FT x &
y in A &
x <> y )
by A9, Def1, Def5;
then
(
y in U_FT x & not
y in {x} &
y in A )
by TARSKI:def 1;
then
(
y in (U_FT x) \ {x} &
y in A )
by XBOOLE_0:def 5;
then
(U_FT x) \ {x} meets A
by XBOOLE_0:3;
hence
x in A ^n
by A8, FIN_TOPO:15;
:: 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