let X be set ; for D being a_partition of X
for P1, P2 being Subset of D st union P1 = union P2 holds
P1 c= P2
let D be a_partition of X; for P1, P2 being Subset of D st union P1 = union P2 holds
P1 c= P2
let P1, P2 be Subset of D; ( union P1 = union P2 implies P1 c= P2 )
assume A1:
union P1 = union P2
; P1 c= P2
let x be object ; TARSKI:def 3 ( not x in P1 or x in P2 )
assume A2:
x in P1
; x in P2
assume A3:
not x in P2
; contradiction
x in D
by A2;
then reconsider x = x as Subset of X ;
A4:
x <> {}
by A2, EQREL_1:def 4;
set a = the Element of x;
the Element of x in union P2
by A1, A2, A4, TARSKI:def 4;
then consider y being set such that
A5:
the Element of x in y
and
A6:
y in P2
by TARSKI:def 4;
A7:
not x misses y
by A4, A5, XBOOLE_0:def 4;
( x in D & y in D )
by A2, A6;
hence
contradiction
by A3, A6, A7, EQREL_1:def 4; verum