let FT be non empty RelStr ; :: thesis: for x being Element of FT
for A being Subset of FT holds
( x in A ^deltai 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) = TRUE ) )

let x be Element of FT; :: thesis: for A being Subset of FT holds
( x in A ^deltai 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) = TRUE ) )

let A be Subset of FT; :: thesis: ( x in A ^deltai 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) = TRUE ) )

A1: ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE implies x in A ^deltai )
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) = TRUE ) ; :: thesis:
then ( x in A ^delta & x in A ) by ;
hence x in A ^deltai by XBOOLE_0:def 4; :: thesis: verum
end;
( x in A ^deltai 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) = TRUE ) )
proof
assume x in A ^deltai ; :: 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) = TRUE )

then ( x in A & x in A ^delta ) by XBOOLE_0:def 4;
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) = TRUE ) by ; :: thesis: verum
end;
hence ( x in A ^deltai 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) = TRUE ) ) by A1; :: thesis: verum