let R be non empty RelStr ; :: thesis: for N being Subset of
for y being Element of st y is_minimal_wrt N,the InternalRel of (R \~ ) holds
not min-classes N is empty
let N be Subset of ; :: thesis: for y being Element of st y is_minimal_wrt N,the InternalRel of (R \~ ) holds
not min-classes N is empty
let y be Element of ; :: thesis: ( y is_minimal_wrt N,the InternalRel of (R \~ ) implies not min-classes N is empty )
assume A1: y is_minimal_wrt N,the InternalRel of (R \~ ) ; :: thesis: not min-classes N is empty
ex x being set st x = (Class (EqRel R),y) /\ N ;
hence not min-classes N is empty by A1, Def8; :: thesis: verum