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