let X be set ; for P being a_partition of X
for x, a, b being set st x in a & a in P & x in b & b in P holds
a = b
let P be a_partition of X; for x, a, b being set st x in a & a in P & x in b & b in P holds
a = b
let x, a, b be set ; ( x in a & a in P & x in b & b in P implies a = b )
assume that
A1:
x in a
and
A2:
a in P
and
A3:
x in b
and
A4:
b in P
; a = b
a meets b
by A1, A3, XBOOLE_0:3;
hence
a = b
by A2, A4, EQREL_1:def 6; verum