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 )

P_1 (x,y,A) = TRUE )

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

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

( x in A ^i implies for y being Element of FT st P_0 (x,y) = TRUE holds
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 )

y in A ;

then U_FT x c= A ;

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

end;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

then
for y being Element of FT st y in U_FT x holds
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;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

y in A ;

then U_FT x c= A ;

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

P_1 (x,y,A) = TRUE )

proof

hence
( x in A ^i iff for y being Element of FT st P_0 (x,y) = TRUE holds
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;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

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