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