let FT be non empty RelStr ; 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; 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; ( 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
;
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
;
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
;
( 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;
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 )
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; verum