let FT be non empty RelStr ; :: thesis: for x being Element of FT

for A being Subset of FT holds

( x in A ^f iff ex y being Element of FT st

( y in A & x in U_FT y ) )

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

( x in A ^f iff ex y being Element of FT st

( y in A & x in U_FT y ) )

let A be Subset of FT; :: thesis: ( x in A ^f iff ex y being Element of FT st

( y in A & x in U_FT y ) )

thus ( x in A ^f implies ex y being Element of FT st

( y in A & x in U_FT y ) ) :: thesis: ( ex y being Element of FT st

( y in A & x in U_FT y ) implies x in A ^f )

( z in A & x in U_FT z ) ; :: thesis: x in A ^f

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

for A being Subset of FT holds

( x in A ^f iff ex y being Element of FT st

( y in A & x in U_FT y ) )

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

( x in A ^f iff ex y being Element of FT st

( y in A & x in U_FT y ) )

let A be Subset of FT; :: thesis: ( x in A ^f iff ex y being Element of FT st

( y in A & x in U_FT y ) )

thus ( x in A ^f implies ex y being Element of FT st

( y in A & x in U_FT y ) ) :: thesis: ( ex y being Element of FT st

( y in A & x in U_FT y ) implies x in A ^f )

proof

assume
ex z being Element of FT st
assume
x in A ^f
; :: thesis: ex y being Element of FT st

( y in A & x in U_FT y )

then ex y being Element of FT st

( y = x & ex z being Element of FT st

( z in A & y in U_FT z ) ) ;

hence ex y being Element of FT st

( y in A & x in U_FT y ) ; :: thesis: verum

end;( y in A & x in U_FT y )

then ex y being Element of FT st

( y = x & ex z being Element of FT st

( z in A & y in U_FT z ) ) ;

hence ex y being Element of FT st

( y in A & x in U_FT y ) ; :: thesis: verum

( z in A & x in U_FT z ) ; :: thesis: x in A ^f

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