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