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