let Y be non empty TopStruct ; :: thesis: for A, B being Subset of Y st ( A is T_0 or B is T_0 ) holds

A /\ B is T_0

let A, B be Subset of Y; :: thesis: ( ( A is T_0 or B is T_0 ) implies A /\ B is T_0 )

assume A1: ( A is T_0 or B is T_0 ) ; :: thesis: A /\ B is T_0

A /\ B is T_0

let A, B be Subset of Y; :: thesis: ( ( A is T_0 or B is T_0 ) implies A /\ B is T_0 )

assume A1: ( A is T_0 or B is T_0 ) ; :: thesis: A /\ B is T_0