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

proof

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:8;
then ( U_FT px meets A or U_FT px meets B ) by XBOOLE_1:70;
then ( x in A ^b or x in B ^b ) by FIN_TOPO:8;
hence x in (A ^b) \/ (B ^b) by XBOOLE_0:def 3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (A ^b) \/ (B ^b) or x in (A \/ B) ^b )
assume A2: x in (A ^b) \/ (B ^b) ; :: thesis: x in (A \/ B) ^b
then reconsider px = x as Point of T ;
( x in A ^b or x in B ^b ) by A2, XBOOLE_0:def 3;
then ( U_FT px meets A or U_FT px meets B ) by FIN_TOPO:8;
then U_FT px meets A \/ B by XBOOLE_1:70;
hence x in (A \/ B) ^b by FIN_TOPO:8; :: thesis: verum