let Y be non empty set ; :: thesis: for PA being a_partition of Y

for X, V being set st X in PA & V in PA & X c= V holds

X = V

let PA be a_partition of Y; :: thesis: for X, V being set st X in PA & V in PA & X c= V holds

X = V

let X, V be set ; :: thesis: ( X in PA & V in PA & X c= V implies X = V )

assume that

A1: X in PA and

A2: V in PA and

A3: X c= V ; :: thesis: X = V

A4: ( X = V or X misses V ) by A1, A2, EQREL_1:def 4;

set x = the Element of X;

X <> {} by A1, EQREL_1:def 4;

then the Element of X in X ;

hence X = V by A3, A4, XBOOLE_0:3; :: thesis: verum

for X, V being set st X in PA & V in PA & X c= V holds

X = V

let PA be a_partition of Y; :: thesis: for X, V being set st X in PA & V in PA & X c= V holds

X = V

let X, V be set ; :: thesis: ( X in PA & V in PA & X c= V implies X = V )

assume that

A1: X in PA and

A2: V in PA and

A3: X c= V ; :: thesis: X = V

A4: ( X = V or X misses V ) by A1, A2, EQREL_1:def 4;

set x = the Element of X;

X <> {} by A1, EQREL_1:def 4;

then the Element of X in X ;

hence X = V by A3, A4, XBOOLE_0:3; :: thesis: verum