let FT be non empty RelStr ; :: thesis: for A being Subset of FT holds A ^delta = (A ^b) /\ ((A ^i) `)

let A be Subset of FT; :: thesis: A ^delta = (A ^b) /\ ((A ^i) `)

for x being object holds

( x in A ^delta iff x in (A ^b) /\ ((A ^i) `) )

let A be Subset of FT; :: thesis: A ^delta = (A ^b) /\ ((A ^i) `)

for x being object holds

( x in A ^delta iff x in (A ^b) /\ ((A ^i) `) )

proof

hence
A ^delta = (A ^b) /\ ((A ^i) `)
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in A ^delta iff x in (A ^b) /\ ((A ^i) `) )

thus ( x in A ^delta implies x in (A ^b) /\ ((A ^i) `) ) :: thesis: ( x in (A ^b) /\ ((A ^i) `) implies x in A ^delta )

then reconsider y = x as Element of FT ;

x in (A ^i) ` by A3, XBOOLE_0:def 4;

then x in (((A `) ^b) `) ` by FIN_TOPO:17;

then A4: U_FT y meets A ` by FIN_TOPO:8;

x in A ^b by A3, XBOOLE_0:def 4;

then U_FT y meets A by FIN_TOPO:8;

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

end;thus ( x in A ^delta implies x in (A ^b) /\ ((A ^i) `) ) :: thesis: ( x in (A ^b) /\ ((A ^i) `) implies x in A ^delta )

proof

assume A3:
x in (A ^b) /\ ((A ^i) `)
; :: thesis: x in A ^delta
assume A1:
x in A ^delta
; :: thesis: x in (A ^b) /\ ((A ^i) `)

then reconsider y = x as Element of FT ;

U_FT y meets A ` by A1, FIN_TOPO:5;

then y in (((A `) ^b) `) ` ;

then A2: y in (A ^i) ` by FIN_TOPO:17;

U_FT y meets A by A1, FIN_TOPO:5;

then y in A ^b ;

hence x in (A ^b) /\ ((A ^i) `) by A2, XBOOLE_0:def 4; :: thesis: verum

end;then reconsider y = x as Element of FT ;

U_FT y meets A ` by A1, FIN_TOPO:5;

then y in (((A `) ^b) `) ` ;

then A2: y in (A ^i) ` by FIN_TOPO:17;

U_FT y meets A by A1, FIN_TOPO:5;

then y in A ^b ;

hence x in (A ^b) /\ ((A ^i) `) by A2, XBOOLE_0:def 4; :: thesis: verum

then reconsider y = x as Element of FT ;

x in (A ^i) ` by A3, XBOOLE_0:def 4;

then x in (((A `) ^b) `) ` by FIN_TOPO:17;

then A4: U_FT y meets A ` by FIN_TOPO:8;

x in A ^b by A3, XBOOLE_0:def 4;

then U_FT y meets A by FIN_TOPO:8;

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