set I = F;
set A = (subrelstr F) opp+id ;
let x, y be Element of ((subrelstr F) opp+id); WAYBEL_0:def 1,WAYBEL_0:def 6 ( not x in [#] ((subrelstr F) opp+id) or not y in [#] ((subrelstr F) opp+id) or ex b1 being Element of the carrier of ((subrelstr F) opp+id) st
( b1 in [#] ((subrelstr F) opp+id) & x <= b1 & y <= b1 ) )
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 that
A3:
x in [#] ((subrelstr F) opp+id)
and
A4:
y in [#] ((subrelstr F) opp+id)
; ex b1 being Element of the carrier of ((subrelstr F) opp+id) st
( b1 in [#] ((subrelstr F) opp+id) & x <= b1 & y <= b1 )
reconsider a = x, b = y as Element of R by A1, A2, A3, A4;
A5:
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
A6:
c in F
and
A7:
a >= c
and
A8:
b >= c
by A1, A2, WAYBEL_0:def 2;
reconsider a1 = x, b1 = y, c1 = c as Element of (subrelstr F) by A6, WAYBEL_9:def 6, YELLOW_0:def 15;
reconsider z = c as Element of ((subrelstr F) opp+id) by A2, A6, YELLOW_0:def 15;
take
z
; ( z in [#] ((subrelstr F) opp+id) & x <= z & y <= z )
A9:
a1 ~ = a1
by LATTICE3:def 6;
A10:
b1 ~ = b1
by LATTICE3:def 6;
A11:
c1 ~ = c1
by LATTICE3:def 6;
A12:
a1 >= c1
by A7, YELLOW_0:60;
A13:
b1 >= c1
by A8, YELLOW_0:60;
A14:
a1 ~ <= c1 ~
by A12, LATTICE3:9;
b1 ~ <= c1 ~
by A13, LATTICE3:9;
hence
( z in [#] ((subrelstr F) opp+id) & x <= z & y <= z )
by A5, A9, A10, A11, A14; verum