set I = F;
set A = (subrelstr F) opp+id ;
let x, y be Element of ((subrelstr F) opp+id ); :: according to WAYBEL_0:def 1,WAYBEL_0:def 6 :: thesis: ( not x in [#] ((subrelstr F) opp+id ) or not y in [#] ((subrelstr F) opp+id ) or ex b₁ being Element of the carrier of ((subrelstr F) opp+id ) st
( b₁ in [#] ((subrelstr F) opp+id ) & x <= b₁ & y <= b₁ ) )
A1: the carrier of (subrelstr F) = F by YELLOW_0:def 15;
A2: the carrier of ((subrelstr F) opp+id ) = the carrier of (subrelstr F) by WAYBEL_9:def 6;
assume ( x in [#] ((subrelstr F) opp+id ) & y in [#] ((subrelstr F) opp+id ) ) ; :: thesis: ex b₁ being Element of the carrier of ((subrelstr F) opp+id ) st
( b₁ in [#] ((subrelstr F) opp+id ) & x <= b₁ & y <= b₁ )
then reconsider a = x, b = y as Element of R by A1, A2;
A3: RelStr(# the carrier of ((subrelstr F) opp+id ),the InternalRel of ((subrelstr F) opp+id ) #) = RelStr(# the carrier of ((subrelstr F) opp ),the InternalRel of ((subrelstr F) opp ) #) by WAYBEL_9:11;
consider c being Element of R such that
A4: ( c in F & a >= c & b >= c ) by A1, A2, WAYBEL_0:def 2;
reconsider a1 = x, b1 = y, c1 = c as Element of (subrelstr F) by A4, WAYBEL_9:def 6, YELLOW_0:def 15;
reconsider z = c as Element of ((subrelstr F) opp+id ) by A2, A4, YELLOW_0:def 15;
take z ; :: thesis: ( z in [#] ((subrelstr F) opp+id ) & x <= z & y <= z )
A5: ( a1 ~ = a1 & b1 ~ = b1 & c1 ~ = c1 ) by LATTICE3:def 6;
( a1 >= c1 & b1 >= c1 ) by A4, YELLOW_0:61;
then ( a1 ~ <= c1 ~ & b1 ~ <= c1 ~ ) by LATTICE3:9;
hence ( z in [#] ((subrelstr F) opp+id ) & x <= z & y <= z ) by A3, A5, YELLOW_0:1; :: thesis: verum