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_maximal_in B holds
y is_maximal_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_maximal_in B holds
y is_maximal_in B
let B be Subset of ; :: thesis: for x being Element of
for y being Element of st x = y & x is_maximal_in B holds
y is_maximal_in B
let x be Element of ; :: thesis: for y being Element of st x = y & x is_maximal_in B holds
y is_maximal_in B
let y be Element of ; :: 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 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 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