take {} ; :: thesis: ( {} is Subset of X & ( for x, y being Point of X st x in {} & y in {} & x <> y holds
x .|. y = 0 ) )
thus ( {} is Subset of X & ( for x, y being Point of X st x in {} & y in {} & x <> y holds
x .|. y = 0 ) ) by SUBSET_1:1; :: thesis: verum