let i, j, n be Nat; ( n = max (i,j) implies square-uparrow n c= (square-uparrow i) /\ (square-uparrow j) )
assume A1:
n = max (i,j)
; square-uparrow n c= (square-uparrow i) /\ (square-uparrow j)
let x be object ; TARSKI:def 3 ( not x in square-uparrow n or x in (square-uparrow i) /\ (square-uparrow j) )
assume A2:
x in square-uparrow n
; x in (square-uparrow i) /\ (square-uparrow j)
then reconsider y = x as Element of [:NAT,NAT:] ;
consider n1, n2 being Nat such that
A3:
n1 = y `1
and
A4:
n2 = y `2
and
A5:
n <= n1
and
A6:
n <= n2
by A2, Def3;
( i <= n & j <= n )
by A1, XXREAL_0:25;
then
( i <= n1 & j <= n1 & i <= n2 & j <= n2 )
by A5, A6, XXREAL_0:2;
then
( y in square-uparrow i & y in square-uparrow j )
by A3, A4, Def3;
hence
x in (square-uparrow i) /\ (square-uparrow j)
by XBOOLE_0:def 4; verum