let R be non empty RelStr ; :: thesis: for N being Subset of R
for x being set st x in min-classes N holds
not x is empty
let N be Subset of R; :: thesis: for x being set st x in min-classes N holds
not x is empty
let x be set ; :: thesis: ( x in min-classes N implies not x is empty )
assume x in min-classes N ; :: thesis: not x is empty
then consider y being Element of (R \~) such that
A1: y is_minimal_wrt N, the InternalRel of (R \~) and
A2: x = (Class ((EqRel R),y)) /\ N by Def8;
A3: y in N by A1, WAYBEL_4:def 25;
y in Class ((EqRel R),y) by EQREL_1:20;
hence not x is empty by A2, A3, XBOOLE_0:def 4; :: thesis: verum