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 object ; :: 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 ;
A2: U_FT px meets A /\ B by A1, FIN_TOPO:8;
then U_FT px meets B by XBOOLE_1:74;
then A3: x in B ^b by FIN_TOPO:8;
U_FT px meets A by A2, XBOOLE_1:74;
then x in A ^b by FIN_TOPO:8;
hence x in (A ^b) /\ (B ^b) by A3, XBOOLE_0:def 4; :: thesis: verum