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 26;
y in Class (EqRel R),y by EQREL_1:28;
hence not x is empty by A2, A3, XBOOLE_0:def 4; :: thesis: verum