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 set ; :: 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 A2: ( x in A ^i & x in B ^i ) by XBOOLE_0:def 4;
reconsider px = x as Point of T by A1;
( U_FT px c= A & U_FT px c= B ) by A2, FIN_TOPO:12;
then U_FT px c= A /\ B by XBOOLE_1:19;
hence x in (A /\ B) ^i by FIN_TOPO:12; :: thesis: verum

end;

let x be set ; :: 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:12;
then A5: U_FT px c= A by XBOOLE_1:18;
U_FT px c= B by A4, XBOOLE_1:18;
then ( x in A ^i & x in B ^i ) by A5, FIN_TOPO:12;
hence x in (A ^i ) /\ (B ^i ) by XBOOLE_0:def 4; :: thesis: verum