take {} ; :: thesis: ( {} is Subset of X & {} is trivial )
thus ( {} is Subset of X & {} is trivial ) by XBOOLE_1:2; :: thesis: verum