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

proof

assume A2: for y being Element of FT st P_0 (x,y) = TRUE holds
P_1 (x,y,A) = TRUE ; :: thesis: x in A ^i
for y being Element of FT st y in U_FT x holds
( y in U_FT x & y in A )

proof

let y be Element of FT; :: thesis: ( y in U_FT x implies ( y in U_FT x & y in A ) )
assume y in U_FT x ; :: thesis: ( y in U_FT x & y in A )
then P_0 (x,y) = TRUE by Def3;
then P_1 (x,y,A) = TRUE by A2;
hence ( y in U_FT x & y in A ) by Def1; :: thesis: verum

end;

then for y being Element of FT st y in U_FT x holds
y in A ;
then U_FT x c= A ;
hence x in A ^i ; :: thesis: verum

end;

( x in A ^i implies for y being Element of FT st P_0 (x,y) = TRUE holds
P_1 (x,y,A) = TRUE )

proof

assume x in A ^i ; :: thesis: for y being Element of FT st P_0 (x,y) = TRUE holds
P_1 (x,y,A) = TRUE
then A3: U_FT x c= A by FIN_TOPO:7;
let y be Element of FT; :: thesis: ( P_0 (x,y) = TRUE implies P_1 (x,y,A) = TRUE )
assume P_0 (x,y) = TRUE ; :: thesis: P_1 (x,y,A) = TRUE
then y in U_FT x by Def3;
hence P_1 (x,y,A) = TRUE by A3, Def1; :: thesis: verum

end;

hence ( x in A ^i iff for y being Element of FT st P_0 (x,y) = TRUE holds
P_1 (x,y,A) = TRUE ) by A1; :: thesis: verum