let T be non empty RelStr ; :: thesis: for A, B being Subset of T holds (A /\ B) ^b c= (A ^b ) /\ (B ^b )
let A, B be Subset of T; :: thesis: (A /\ B) ^b c= (A ^b ) /\ (B ^b )
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (A /\ B) ^b or x in (A ^b ) /\ (B ^b ) )
assume A1: x in (A /\ B) ^b ; :: thesis: x in (A ^b ) /\ (B ^b )
then reconsider px = x as Point of T ;
U_FT px meets A /\ B by A1, FIN_TOPO:13;
then ( U_FT px meets A & U_FT px meets B ) by XBOOLE_1:74;
then ( x in A ^b & x in B ^b ) by FIN_TOPO:13;
hence x in (A ^b ) /\ (B ^b ) by XBOOLE_0:def 4; :: thesis: verum