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

proof

reconsider z = x as Element of FT ;
assume A2: x in A ^delta ; :: thesis: ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE )
then U_FT z meets A by FIN_TOPO:5;
then consider w1 being object such that
A3: w1 in U_FT z and
A4: w1 in A by XBOOLE_0:3;
reconsider w1 = w1 as Element of FT by A3;
take w1 ; :: thesis: ex y2 being Element of FT st
( P_1 (x,w1,A) = TRUE & P_2 (x,y2,A) = TRUE )
U_FT z meets A ` by A2, FIN_TOPO:5;
then consider w2 being object such that
A5: ( w2 in U_FT z & w2 in A ` ) by XBOOLE_0:3;
take w2 ; :: thesis: ( w2 is set & w2 is Element of FT & P_1 (x,w1,A) = TRUE & P_2 (x,w2,A) = TRUE )
thus ( w2 is set & w2 is Element of FT & P_1 (x,w1,A) = TRUE & P_2 (x,w2,A) = TRUE ) by A3, A4, A5, Def1, Def2; :: thesis: verum

end;

( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) implies x in A ^delta )

proof

given y1, y2 being Element of FT such that A6: P_1 (x,y1,A) = TRUE and
A7: P_2 (x,y2,A) = TRUE ; :: thesis: x in A ^delta
( y1 in U_FT x & y1 in A ) by A6, Def1;
then (U_FT x) /\ A <> {} by XBOOLE_0:def 4;
then A8: U_FT x meets A ;
( y2 in U_FT x & y2 in A ` ) by A7, Def2;
then U_FT x meets A ` by XBOOLE_0:3;
hence x in A ^delta by A8; :: thesis: verum

end;

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