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
ex x being set st x = (Class ((EqRel R),y)) /\ N ;
hence not min-classes N is empty by A1, Def8; :: thesis: verum