let R be non empty RelStr ; :: thesis: for N being Subset of R
for y being Element of (R \~ ) st y is_minimal_wrt N,the InternalRel of (R \~ ) holds
not min-classes N is empty
let N be Subset of R; :: thesis: for y being Element of (R \~ ) st y is_minimal_wrt N,the InternalRel of (R \~ ) holds
not min-classes N is empty
let y be Element of (R \~ ); :: 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
consider x being set such that
A2: x = (Class (EqRel R),y) /\ N ;
thus not min-classes N is empty by A1, A2, Def8; :: thesis: verum