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

hereby :: thesis: verum

per cases ( A is T_0 or B is T_0 ) by A1;

suppose A is T_0 ; :: thesis: A /\ B is T_0

hence A /\ B is T_0 by Th7, XBOOLE_1:17; :: thesis: verum

end;

suppose B is T_0 ; :: thesis: A /\ B is T_0

hence A /\ B is T_0 by Th7, XBOOLE_1:17; :: thesis: verum

end;

end;

end;