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

assume A2: x in A ^b ; :: thesis: ex y1 being Element of FT st P_1 x,y1,A = TRUE
reconsider z = x as Element of FT ;
U_FT z meets A by A2, FIN_TOPO:13;
then consider w being set such that
A3: ( w in U_FT z & w in A ) by XBOOLE_0:3;
reconsider w = w as Element of FT by A3;
take w ; :: thesis: P_1 x,w,A = TRUE
thus P_1 x,w,A = TRUE by 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 by XBOOLE_0:def 7;
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