set X = { F₅(i) where i is Element of F₃() : ex l being Instruction-Location of F₄() st
( l = F₆() & P₁[i,l] ) } ;
set Y = { F₅(j) where j is Element of F₃() : P₁[j,F₆()] } ;
thus { F₅(i) where i is Element of F₃() : ex l being Instruction-Location of F₄() st
( l = F₆() & P₁[i,l] ) } c= { F₅(j) where j is Element of F₃() : P₁[j,F₆()] } :: according to XBOOLE_0:def 10 :: thesis: { F₅(j) where j is Element of F₃() : P₁[j,F₆()] } c= { F₅(i) where i is Element of F₃() : ex l being Instruction-Location of F₄() st
( l = F₆() & P₁[i,l] ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₅(i) where i is Element of F₃() : ex l being Instruction-Location of F₄() st
( l = F₆() & P₁[i,l] ) } or x in { F₅(j) where j is Element of F₃() : P₁[j,F₆()] } )
assume x in { F₅(i) where i is Element of F₃() : ex l being Instruction-Location of F₄() st
( l = F₆() & P₁[i,l] ) } ; :: thesis: x in { F₅(j) where j is Element of F₃() : P₁[j,F₆()] }
then ex i being Element of F₃() st
( x = F₅(i) & ex l being Instruction-Location of F₄() st
( l = F₆() & P₁[i,l] ) ) ;
hence x in { F₅(j) where j is Element of F₃() : P₁[j,F₆()] } ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₅(j) where j is Element of F₃() : P₁[j,F₆()] } or x in { F₅(i) where i is Element of F₃() : ex l being Instruction-Location of F₄() st
( l = F₆() & P₁[i,l] ) } )
assume x in { F₅(j) where j is Element of F₃() : P₁[j,F₆()] } ; :: thesis: x in { F₅(i) where i is Element of F₃() : ex l being Instruction-Location of F₄() st
( l = F₆() & P₁[i,l] ) }
then ex j being Element of F₃() st
( x = F₅(j) & P₁[j,F₆()] ) ;
hence x in { F₅(i) where i is Element of F₃() : ex l being Instruction-Location of F₄() st
( l = F₆() & P₁[i,l] ) } ; :: thesis: verum