let FT be non empty RelStr ; :: thesis: for A, B being Subset of FT holds (A \/ B) ^b = (A ^b) \/ (B ^b)
let A, B be Subset of FT; :: thesis: (A \/ B) ^b = (A ^b) \/ (B ^b)
A1: (A \/ B) ^b c= (A ^b) \/ (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 x in (A \/ B) ^b ; :: thesis: x in (A ^b) \/ (B ^b)
then consider y being Element of FT such that
A2: x = y and
A3: U_FT y meets A \/ B ;
( U_FT y meets A or U_FT y meets B ) by A3, XBOOLE_1:70;
then ( x in { u where u is Element of FT : U_FT u meets A } or x in B ^b ) by A2;
hence x in (A ^b) \/ (B ^b) by XBOOLE_0:def 3; :: thesis: verum

end;

( A ^b c= (A \/ B) ^b & B ^b c= (A \/ B) ^b ) by FIN_TOPO:14, XBOOLE_1:7;
then (A ^b) \/ (B ^b) c= (A \/ B) ^b by XBOOLE_1:8;
hence (A \/ B) ^b = (A ^b) \/ (B ^b) by A1, XBOOLE_0:def 10; :: thesis: verum