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 ( U_FT x meets A & U_FT x meets A ` ) )

let x be Element of FT; :: thesis: for A being Subset of FT holds

( x in A ^delta iff ( U_FT x meets A & U_FT x meets A ` ) )

let A be Subset of FT; :: thesis: ( x in A ^delta iff ( U_FT x meets A & U_FT x meets A ` ) )

thus ( x in A ^delta implies ( U_FT x meets A & U_FT x meets A ` ) ) :: thesis: ( U_FT x meets A & U_FT x meets A ` implies x in A ^delta )

hence x in A ^delta ; :: thesis: verum

for A being Subset of FT holds

( x in A ^delta iff ( U_FT x meets A & U_FT x meets A ` ) )

let x be Element of FT; :: thesis: for A being Subset of FT holds

( x in A ^delta iff ( U_FT x meets A & U_FT x meets A ` ) )

let A be Subset of FT; :: thesis: ( x in A ^delta iff ( U_FT x meets A & U_FT x meets A ` ) )

thus ( x in A ^delta implies ( U_FT x meets A & U_FT x meets A ` ) ) :: thesis: ( U_FT x meets A & U_FT x meets A ` implies x in A ^delta )

proof

assume
( U_FT x meets A & U_FT x meets A ` )
; :: thesis: x in A ^delta
assume
x in A ^delta
; :: thesis: ( U_FT x meets A & U_FT x meets A ` )

then ex y being Element of FT st

( y = x & U_FT y meets A & U_FT y meets A ` ) ;

hence ( U_FT x meets A & U_FT x meets A ` ) ; :: thesis: verum

end;then ex y being Element of FT st

( y = x & U_FT y meets A & U_FT y meets A ` ) ;

hence ( U_FT x meets A & U_FT x meets A ` ) ; :: thesis: verum

hence x in A ^delta ; :: thesis: verum