let x, y be Element of (subrelstr I); :: according to WAYBEL_0:def 1,WAYBEL_0:def 6 :: thesis: ( not x in [#] (subrelstr I) or not y in [#] (subrelstr I) or ex b₁ being Element of the carrier of (subrelstr I) st
( b₁ in [#] (subrelstr I) & x <= b₁ & y <= b₁ ) )
A1: the carrier of (subrelstr I) = I by YELLOW_0:def 15;
assume that
A2: x in [#] (subrelstr I) and
A3: y in [#] (subrelstr I) ; :: thesis: ex b₁ being Element of the carrier of (subrelstr I) st
( b₁ in [#] (subrelstr I) & x <= b₁ & y <= b₁ )
reconsider a = x, b = y as Element of R by A1, A2, A3;
consider c being Element of R such that
A4: c in I and
A5: a <= c and
A6: b <= c by A1, A2, WAYBEL_0:def 1;
reconsider z = c as Element of (subrelstr I) by A4, YELLOW_0:def 15;
take z ; :: thesis: ( z in [#] (subrelstr I) & x <= z & y <= z )
thus ( z in [#] (subrelstr I) & x <= z & y <= z ) by A2, A5, A6, YELLOW_0:60; :: thesis: verum