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
A: x = y and
B: x is_minimal_in B ; :: thesis: y is_minimal_in B
C: x in B by B, WAYBEL_4:57;
assume not y is_minimal_in B ; :: thesis: contradiction
then consider z being Element of R such that
A1: z in B and
B1: z < y by A, C, WAYBEL_4:57;
C1: z <= y by B1, ORDERS_2:def 10;
reconsider z9 = z as Element of (subrelstr S) by A1;
z9 <= x by A1, C1, A, YELLOW_0:61;
then z9 < x by B1, A, ORDERS_2:def 10;
hence contradiction by A1, B, WAYBEL_4:57; :: thesis: verum