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

( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) implies x in A ^n )

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

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

( P_A (x,A) = TRUE & ex y being Element of FT st
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 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; :: thesis: verum

end;( 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; :: thesis: verum

( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) implies x in A ^n )

proof

hence
( x in A ^n iff ( P_A (x,A) = TRUE & ex y being Element of FT st
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 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; :: thesis: verum

end;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 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; :: thesis: verum

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