let R be RelStr ; :: thesis: for S being Subset of R
for B being Subset of (subrelstr S)
for x being Element of (subrelstr S)
for y being Element of R st x = y & x is_minimal_in B holds
y is_minimal_in B
let S be Subset of R; :: thesis: for B being Subset of (subrelstr S)
for x being Element of (subrelstr S)
for y being Element of R st x = y & x is_minimal_in B holds
y is_minimal_in B
let B be Subset of (subrelstr S); :: thesis: for x being Element of (subrelstr S)
for y being Element of R st x = y & x is_minimal_in B holds
y is_minimal_in B
let x be Element of (subrelstr S); :: thesis: for y being Element of R st x = y & x is_minimal_in B holds
y is_minimal_in B
let y be Element of R; :: thesis: ( x = y & x is_minimal_in B implies y is_minimal_in B )
assume that
A1: x = y and
A2: x is_minimal_in B ; :: thesis: y is_minimal_in B
A3: x in B by A2, WAYBEL_4:56;
assume not y is_minimal_in B ; :: thesis: contradiction
then consider z being Element of R such that
A4: z in B and
A5: z < y by A1, A3, WAYBEL_4:56;
A6: z <= y by A5, ORDERS_2:def 6;
reconsider z9 = z as Element of (subrelstr S) by A4;
z9 <= x by A4, A6, A1, YELLOW_0:60;
then z9 < x by A5, A1, ORDERS_2:def 6;
hence contradiction by A4, A2, WAYBEL_4:56; :: thesis: verum