let FT be non empty RelStr ; :: thesis: for A being Subset of FT holds A ^delta = (A ^b) /\ ((A `) ^b)
let A be Subset of FT; :: thesis: A ^delta = (A ^b) /\ ((A `) ^b)
for x being object holds
( x in A ^delta iff x in (A ^b) /\ ((A `) ^b) )
proof
let x be object ; :: thesis: ( x in A ^delta iff x in (A ^b) /\ ((A `) ^b) )
thus ( x in A ^delta implies x in (A ^b) /\ ((A `) ^b) ) :: thesis: ( x in (A ^b) /\ ((A `) ^b) implies x in A ^delta )
proof
assume A1: x in A ^delta ; :: thesis: x in (A ^b) /\ ((A `) ^b)
then reconsider y = x as Element of FT ;
U_FT y meets A ` by ;
then A2: x in (A `) ^b ;
U_FT y meets A by ;
then x in A ^b ;
hence x in (A ^b) /\ ((A `) ^b) by ; :: thesis: verum
end;
assume A3: x in (A ^b) /\ ((A `) ^b) ; :: thesis: x in A ^delta
then reconsider y = x as Element of FT ;
x in (A `) ^b by ;
then A4: U_FT y meets A ` by Th8;
x in A ^b by ;
then U_FT y meets A by Th8;
hence x in A ^delta by A4; :: thesis: verum
end;
hence A ^delta = (A ^b) /\ ((A `) ^b) by TARSKI:2; :: thesis: verum