let R be RelStr ; :: thesis: for S being Subset of
for B being Subset of
for x being Element of
for y being Element of st x = y & x is_minimal_in B holds
y is_minimal_in B
let S be Subset of ; :: thesis: for B being Subset of
for x being Element of
for y being Element of st x = y & x is_minimal_in B holds
y is_minimal_in B
let B be Subset of ; :: thesis: for x being Element of
for y being Element of st x = y & x is_minimal_in B holds
y is_minimal_in B
let x be Element of ; :: thesis: for y being Element of st x = y & x is_minimal_in B holds
y is_minimal_in B
let y be Element of ; :: 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 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 z' = z as Element of by A1;
z' <= x by A1, C1, A, YELLOW_0:61;
then z' < x by B1, A, ORDERS_2:def 10;
hence contradiction by A1, B, WAYBEL_4:57; :: thesis: verum