let T be non empty RelStr ; :: thesis: for A, B being Subset of T holds (A ^f) \/ (B ^f) = (A \/ B) ^f
let A, B be Subset of T; :: thesis: (A ^f) \/ (B ^f) = (A \/ B) ^f
( A ^f c= (A \/ B) ^f & B ^f c= (A \/ B) ^f ) by Th5, XBOOLE_1:7;
hence (A ^f) \/ (B ^f) c= (A \/ B) ^f by XBOOLE_1:8; :: according to XBOOLE_0:def 10 :: thesis: (A \/ B) ^f c= (A ^f) \/ (B ^f)
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in (A \/ B) ^f or z in (A ^f) \/ (B ^f) )
assume z in (A \/ B) ^f ; :: thesis: z in (A ^f) \/ (B ^f)
then consider y being Element of T such that
A1: y in A \/ B and
A2: z in U_FT y by FIN_TOPO:11;

per cases ( y in A or y in B ) by A1, XBOOLE_0:def 3;

suppose y in A ; :: thesis: z in (A ^f) \/ (B ^f)

then z in A ^f by A2, FIN_TOPO:11;
hence z in (A ^f) \/ (B ^f) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose y in B ; :: thesis: z in (A ^f) \/ (B ^f)

then z in B ^f by A2, FIN_TOPO:11;
hence z in (A ^f) \/ (B ^f) by XBOOLE_0:def 3; :: thesis: verum

end;

end;