let FT be non empty RelStr ; :: thesis: for x being Element of FT
for A being Subset of FT holds
( x in A ^f iff ex y being Element of FT st
( P_A y,A = TRUE & P_0 y,x = TRUE ) )
let x be Element of FT; :: thesis: for A being Subset of FT holds
( x in A ^f iff ex y being Element of FT st
( P_A y,A = TRUE & P_0 y,x = TRUE ) )
let A be Subset of FT; :: thesis: ( x in A ^f iff ex y being Element of FT st
( P_A y,A = TRUE & P_0 y,x = TRUE ) )
A1: ( x in A ^f implies ex y being Element of FT st
( P_A y,A = TRUE & P_0 y,x = TRUE ) )

proof

assume x in A ^f ; :: thesis: ex y being Element of FT st
( P_A y,A = TRUE & P_0 y,x = TRUE )
then consider y being Element of FT such that
A2: ( y in A & x in U_FT y ) by FIN_TOPO:16;
A3: P_A y,A = TRUE by A2, Def4;
P_0 y,x = TRUE by A2, Def3;
hence ex y being Element of FT st
( P_A y,A = TRUE & P_0 y,x = TRUE ) by A3; :: thesis: verum

end;

( ex y being Element of FT st
( P_A y,A = TRUE & P_0 y,x = TRUE ) implies x in A ^f )

proof

assume ex y being Element of FT st
( P_A y,A = TRUE & P_0 y,x = TRUE ) ; :: thesis: x in A ^f
then consider y being Element of FT such that
A4: ( P_A y,A = TRUE & P_0 y,x = TRUE ) ;
A5: y in A by A4, Def4;
x in U_FT y by A4, Def3;
hence x in A ^f by A5; :: thesis: verum

end;

hence ( x in A ^f iff ex y being Element of FT st
( P_A y,A = TRUE & P_0 y,x = TRUE ) ) by A1; :: thesis: verum