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

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