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