let T be TopStruct ; :: thesis: for F, G being Subset-Family of T st F is open & G is open holds
F \/ G is open
let F, G be Subset-Family of T; :: thesis: ( F is open & G is open implies F \/ G is open )
assume A1: ( F is open & G is open ) ; :: thesis: F \/ G is open
let P be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( P in F \/ G implies P is open )
assume P in F \/ G ; :: thesis: P is open
then ( P in F or P in G ) by XBOOLE_0:def 3;
hence P is open by A1; :: thesis: verum