let T be TopSpace; :: thesis: for G, G1 being Subset-Family of T
for i being Integer st G is finite-ind & G1 is finite-ind & ind G <= i & ind G1 <= i holds
( G \/ G1 is finite-ind & ind (G \/ G1) <= i )
let G, G1 be Subset-Family of T; :: thesis: for i being Integer st G is finite-ind & G1 is finite-ind & ind G <= i & ind G1 <= i holds
( G \/ G1 is finite-ind & ind (G \/ G1) <= i )
let i be Integer; :: thesis: ( G is finite-ind & G1 is finite-ind & ind G <= i & ind G1 <= i implies ( G \/ G1 is finite-ind & ind (G \/ G1) <= i ) )
assume that
A1: G is finite-ind and
A2: G1 is finite-ind and
A3: ind G <= i and
A4: ind G1 <= i ; :: thesis: ( G \/ G1 is finite-ind & ind (G \/ G1) <= i )
A5: for A being Subset of T st A in G \/ G1 holds
( A is finite-ind & ind A <= i )

proof

let A be Subset of T; :: thesis: ( A in G \/ G1 implies ( A is finite-ind & ind A <= i ) )
assume A in G \/ G1 ; :: thesis: ( A is finite-ind & ind A <= i )
then ( A in G or A in G1 ) by XBOOLE_0:def 3;
hence ( A is finite-ind & ind A <= i ) by A1, A2, A3, A4, Th11; :: thesis: verum

end;

- 1 <= i by A1, A3, Th11;
hence ( G \/ G1 is finite-ind & ind (G \/ G1) <= i ) by A5, Th11; :: thesis: verum