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_maximal_in B holds
y is_maximal_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_maximal_in B holds
y is_maximal_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_maximal_in B holds
y is_maximal_in B
let x be Element of (subrelstr S); :: thesis: for y being Element of R st x = y & x is_maximal_in B holds
y is_maximal_in B
let y be Element of R; :: thesis: ( x = y & x is_maximal_in B implies y is_maximal_in B )
assume that
A1: x = y and
A2: x is_maximal_in B ; :: thesis: y is_maximal_in B
A3: x in B by A2, WAYBEL_4:55;
assume not y is_maximal_in B ; :: thesis: contradiction
then consider z being Element of R such that
A4: z in B and
A5: y < z by A1, A3, WAYBEL_4:55;
A6: y <= z by A5, ORDERS_2:def 6;
reconsider z9 = z as Element of (subrelstr S) by A4;
x <= z9 by A4, A6, A1, YELLOW_0:60;
then x < z9 by A5, A1, ORDERS_2:def 6;
hence contradiction by A4, A2, WAYBEL_4:55; :: thesis: verum