let X, x be set ; :: thesis: ( X <> {} implies ( [:{x},X:] <> {} & [:X,{x}:] <> {} ) )
assume X <> {} ; :: thesis: ( [:{x},X:] <> {} & [:X,{x}:] <> {} )
then ex y being set st y in X by XBOOLE_0:7;
hence ( [:{x},X:] <> {} & [:X,{x}:] <> {} ) by Th128, Th129; :: thesis: verum