let Q be co-well_founded Relation; :: thesis: for R being Relation st R c= Q holds
R is co-well_founded
let R be Relation; :: thesis: ( R c= Q implies R is co-well_founded )
assume A1: R c= Q ; :: thesis: R is co-well_founded
then A2: field R c= field Q by RELAT_1:31;
let Y be set ; :: according to REWRITE1:def 16 :: thesis: ( Y c= field R & Y <> {} implies ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) ) )
assume A3: ( Y c= field R & Y <> {} ) ; :: thesis: ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) )
then Y c= field Q by A2, XBOOLE_1:1;
then consider a being set such that
A4: a in Y and
A5: for b being set st b in Y & a <> b holds
not [a,b] in Q by A3, Def16;
take a ; :: thesis: ( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) )
thus a in Y by A4; :: thesis: for b being set st b in Y & a <> b holds
not [a,b] in R
let b be set ; :: thesis: ( b in Y & a <> b implies not [a,b] in R )
assume ( b in Y & a <> b ) ; :: thesis: not [a,b] in R
hence not [a,b] in R by A1, A5; :: thesis: verum