let T be non empty RelStr ; :: thesis: for A, B being Subset of T holds (A ^i) \/ (B ^i) c= (A \/ B) ^i
let A, B be Subset of T; :: thesis: (A ^i) \/ (B ^i) c= (A \/ B) ^i
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A ^i) \/ (B ^i) or x in (A \/ B) ^i )
assume A1: x in (A ^i) \/ (B ^i) ; :: thesis: x in (A \/ B) ^i
then reconsider px = x as Point of T ;
( x in A ^i or x in B ^i ) by A1, XBOOLE_0:def 3;
then A2: ( U_FT px c= A or U_FT px c= B ) by FIN_TOPO:7;
( A c= A \/ B & B c= A \/ B ) by XBOOLE_1:7;
then U_FT px c= A \/ B by A2;
hence x in (A \/ B) ^i by FIN_TOPO:7; :: thesis: verum