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
let Y be set ; :: according to REWRITE1:def 16 :: thesis: ( Y c= field R & Y <> {} implies ex a being object st
( a in Y & ( for b being object st b in Y & a <> b holds
not [a,b] in R ) ) )
assume that
A2: Y c= field R and
A3: Y <> {} ; :: thesis: ex a being object st
( a in Y & ( for b being object st b in Y & a <> b holds
not [a,b] in R ) )
field R c= field Q by A1, RELAT_1:16;
then Y c= field Q by A2;
then consider a being object such that
A4: a in Y and
A5: for b being object st b in Y & a <> b holds
not [a,b] in Q by A3, Def16;
take a ; :: thesis: ( a in Y & ( for b being object st b in Y & a <> b holds
not [a,b] in R ) )
thus a in Y by A4; :: thesis: for b being object st b in Y & a <> b holds
not [a,b] in R
let b be object ; :: 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