let i, j, n be Nat; :: thesis: ( n = max (i,j) implies square-uparrow n c= (square-uparrow i) /\ (square-uparrow j) )
assume A1: n = max (i,j) ; :: thesis: square-uparrow n c= (square-uparrow i) /\ (square-uparrow j)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in square-uparrow n or x in (square-uparrow i) /\ (square-uparrow j) )
assume A2: x in square-uparrow n ; :: thesis: 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; :: thesis: verum