let T be non empty RelStr ; :: thesis: for A, B being Subset of T holds (A ^i) /\ (B ^i) = (A /\ B) ^i
let A, B be Subset of T; :: thesis: (A ^i) /\ (B ^i) = (A /\ B) ^i
thus (A ^i) /\ (B ^i) c= (A /\ B) ^i :: according to XBOOLE_0:def 10 :: thesis: (A /\ B) ^i c= (A ^i) /\ (B ^i)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A ^i) /\ (B ^i) or x in (A /\ B) ^i )
assume A1: x in (A ^i) /\ (B ^i) ; :: thesis: x in (A /\ B) ^i
then reconsider px = x as Point of T ;
x in B ^i by A1, XBOOLE_0:def 4;
then A2: U_FT px c= B by FIN_TOPO:7;
x in A ^i by A1, XBOOLE_0:def 4;
then U_FT px c= A by FIN_TOPO:7;
then U_FT px c= A /\ B by A2, XBOOLE_1:19;
hence x in (A /\ B) ^i by FIN_TOPO:7; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A /\ B) ^i or x in (A ^i) /\ (B ^i) )
assume A3: x in (A /\ B) ^i ; :: thesis: x in (A ^i) /\ (B ^i)
then reconsider px = x as Point of T ;
A4: U_FT px c= A /\ B by A3, FIN_TOPO:7;
then U_FT px c= B by XBOOLE_1:18;
then A5: x in B ^i by FIN_TOPO:7;
U_FT px c= A by A4, XBOOLE_1:18;
then x in A ^i by FIN_TOPO:7;
hence x in (A ^i) /\ (B ^i) by A5, XBOOLE_0:def 4; :: thesis: verum