let P be PNPair; :: thesis: rng P c= union (Subt (rng P))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng P or x in union (Subt (rng P)) )
assume A1: x in rng P ; :: thesis: x in union (Subt (rng P))
then reconsider x1 = x as Element of LTLB_WFF ;
A2: ( x in tau1 . x1 & tau1 . x1 c= Sub . x1 ) by LTLAXIO3:6, LTLAXIO3:25;
Sub . x1 in Subt (rng P) by A1;
hence x in union (Subt (rng P)) by A2, TARSKI:def 4; :: thesis: verum