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 A2: ( x in [#] (subrelstr I) & y in [#] (subrelstr I) ) ; :: thesis: ex b₁ being Element of the carrier of (subrelstr I) st
( b₁ in [#] (subrelstr I) & x <= b₁ & y <= b₁ )
then reconsider a = x, b = y as Element of R by A1;
consider c being Element of R such that
A3: ( c in I & a <= c & b <= c ) by A1, A2, WAYBEL_0:def 1;
reconsider z = c as Element of (subrelstr I) by A3, 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, A3, YELLOW_0:61; :: thesis: verum