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 A1: ( X in PA & V in PA & X c= V ) ; :: thesis: X = V
then A2: ( X = V or X misses V ) by EQREL_1:def 6;
consider x being Element of X;
X <> {} by A1, EQREL_1:def 6;
then x in X ;
hence X = V by A1, A2, XBOOLE_0:3; :: thesis: verum