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
A1: A ^f c= (A \/ B) ^f by Th5, XBOOLE_1:7;
B ^f c= (A \/ B) ^f by Th5, XBOOLE_1:7;
hence (A ^f ) \/ (B ^f ) c= (A \/ B) ^f by A1, XBOOLE_1:8; :: according to XBOOLE_0:def 10 :: thesis: (A \/ B) ^f c= (A ^f ) \/ (B ^f )
let z be set ; :: 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
A2: ( y in A \/ B & z in U_FT y ) by FIN_TOPO:16;

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

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

then z in A ^f by A2, FIN_TOPO:16;
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:16;
hence z in (A ^f ) \/ (B ^f ) by XBOOLE_0:def 3; :: thesis: verum

end;

end;