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