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

proof

reconsider z = x as Element of FT ;
assume x in A ^b ; :: thesis: ex y1 being Element of FT st P_1 (x,y1,A) = TRUE
then U_FT z meets A by FIN_TOPO:8;
then consider w being object such that
A2: w in U_FT z and
A3: w in A by XBOOLE_0:3;
reconsider w = w as Element of FT by A2;
take w ; :: thesis: P_1 (x,w,A) = TRUE
thus P_1 (x,w,A) = TRUE by A2, A3, Def1; :: thesis: verum

end;

( ex y1 being Element of FT st P_1 (x,y1,A) = TRUE implies x in A ^b )

proof

given y being Element of FT such that A4: P_1 (x,y,A) = TRUE ; :: thesis: x in A ^b
( y in U_FT x & y in A ) by A4, Def1;
then y in (U_FT x) /\ A by XBOOLE_0:def 4;
then U_FT x meets A ;
hence x in A ^b ; :: thesis: verum

end;

hence ( x in A ^b iff ex y1 being Element of FT st P_1 (x,y1,A) = TRUE ) by A1; :: thesis: verum