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 set ; :: 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 A2: ( x in A ^i or x in B ^i ) by XBOOLE_0:def 3;
reconsider px = x as Point of T by A1;
( ( U_FT px c= A or U_FT px c= B ) & A c= A \/ B & B c= A \/ B ) by A2, FIN_TOPO:12, XBOOLE_1:7;
then U_FT px c= A \/ B by XBOOLE_1:1;
hence x in (A \/ B) ^i by FIN_TOPO:12; :: thesis: verum