let t be Tree; for p, q being FinSequence of NAT st p ^ q in t holds
t | (p ^ q) = (t | p) | q
let p, q be FinSequence of NAT ; ( p ^ q in t implies t | (p ^ q) = (t | p) | q )
assume A1:
p ^ q in t
; t | (p ^ q) = (t | p) | q
let r be FinSequence of NAT ; TREES_2:def 1 ( ( not r in t | (p ^ q) or r in (t | p) | q ) & ( not r in (t | p) | q or r in t | (p ^ q) ) )
A2:
p in t
by A1, TREES_1:21;
then
q in t | p
by A1, TREES_1:def 6;
then A3:
( r in (t | p) | q iff q ^ r in t | p )
by TREES_1:def 6;
A4:
(p ^ q) ^ r = p ^ (q ^ r)
by FINSEQ_1:32;
( r in t | (p ^ q) iff (p ^ q) ^ r in t )
by A1, TREES_1:def 6;
hence
( ( not r in t | (p ^ q) or r in (t | p) | q ) & ( not r in (t | p) | q or r in t | (p ^ q) ) )
by A2, A4, A3, TREES_1:def 6; verum