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: ( ex y being Element of FT st

( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) implies x in A ^f )

( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) )

( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) ) by A1; :: thesis: verum

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: ( ex y being Element of FT st

( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) implies x in A ^f )

proof

( x in A ^f implies ex y being Element of FT st
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

A2: ( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) ;

( y in A & x in U_FT y ) by A2, Def3, Def4;

hence x in A ^f ; :: thesis: verum

end;( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) ; :: thesis: x in A ^f

then consider y being Element of FT such that

A2: ( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) ;

( y in A & x in U_FT y ) by A2, Def3, Def4;

hence x in A ^f ; :: thesis: verum

( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) )

proof

hence
( x in A ^f iff ex y being Element of FT st
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

A3: ( y in A & x in U_FT y ) by FIN_TOPO:11;

( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) by A3, Def3, Def4;

hence ex y being Element of FT st

( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) ; :: thesis: verum

end;( P_A (y,A) = TRUE & P_0 (y,x) = TRUE )

then consider y being Element of FT such that

A3: ( y in A & x in U_FT y ) by FIN_TOPO:11;

( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) by A3, Def3, Def4;

hence ex y being Element of FT st

( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) ; :: thesis: verum

( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) ) by A1; :: thesis: verum