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

proof

assume x in A ^deltao ; :: thesis: ( ex y1, y2 being Element of FT st
( P_1 x,y1,A = TRUE & P_2 x,y2,A = TRUE ) & P_A x,A = FALSE )
then ( x in A ` & x in A ^delta ) by XBOOLE_0:def 4;
then ( not x in A & x in A ^delta ) by XBOOLE_0:def 5;
hence ( ex y1, y2 being Element of FT st
( P_1 x,y1,A = TRUE & P_2 x,y2,A = TRUE ) & P_A x,A = FALSE ) by Def4, Th8; :: thesis: verum

end;

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

proof

assume ( ex y1, y2 being Element of FT st
( P_1 x,y1,A = TRUE & P_2 x,y2,A = TRUE ) & P_A x,A = FALSE ) ; :: thesis: x in A ^deltao
then ( x in A ^delta & x in the carrier of FT & not x in A ) by Def4, Th8;
then ( x in A ^delta & x in A ` ) by XBOOLE_0:def 5;
hence x in A ^deltao by XBOOLE_0:def 4; :: thesis: verum

end;

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