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: ( 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 A2: x in A ^i ; :: thesis: for y being Element of FT st P_0 x,y = TRUE holds
P_1 x,y,A = TRUE
let y be Element of FT; :: thesis: ( P_0 x,y = TRUE implies P_1 x,y,A = TRUE )
assume A3: P_0 x,y = TRUE ; :: thesis: P_1 x,y,A = TRUE
A4: U_FT x c= A by A2, FIN_TOPO:12;
y in U_FT x by A3, Def3;
hence P_1 x,y,A = TRUE by A4, Def1; :: thesis: verum

end;

( ( 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 A5: 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 A5;
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 by SUBSET_1:7;
hence x in A ^i ; :: 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